	*Mathematica*

		Fast Dense Numerical Linear Algebra
		High-Speed Sparse Linear Algebra
		Large-Scale Linear Systems
		Big-Number Arithmetic
		64-Bit Platform Support
		Faster MathLink
		Numerical Solving of Differential Equations
		Numerical Equation Solving
		Fitting Data
		Numeric Optimization
		`DSolve`
		`RSolve`
		`Reduce`
		`Resolve`
		`FindInstance`
		Symbolic Global Optimization
		Wider Support For Domain Specifications
		Connection Technology
		Importing and Exporting
		Statistical Plots
		Collecting Expressions During Evaluation
		New Linear Algebra Functions
		Algebraic Number Objects
		Authoring and Presentation
		Summary of New Features

Ask about this page

Resolve

The function Resolve can eliminate quantifiers (for example and ) from arbitrary polynomial systems in complex or real variables using the same methods used by the solving function Reduce. For cases in which obtaining an implicit quantifier-free form of the system is easier than computing explicit solutions, Resolve returns the implicit form. Resolve can also eliminate quantifiers involving Boolean variables.

Example: Coefficients satisfying constraints

This gives the conditions that real coefficients a, b, and c have to satisfy so that a quadratic polynomial in a real variable x is positive.

$Resolve[ [ForAll]_(x_1 {x_1 a_1 b_1 c} [ElementOf] R) c x^2 + b x + a [GreaterThan] 0]$

Example: Does x² + y² < 1 Imply that y > x⁴ - 2?

Graphically, the above result means that the unit circle lies inside the parabola.

		Documentation from The Mathematica Book Advanced Topic: Quantifiers

		Documentation from the Reference Guide `Resolve` `Reduce` `Implies`