Real Closed Fields

Simplification#

This module implements deep simplification for Real Closed Fields by generating and propagating internal representations during recursion. It extends the standard simplifier for Ordered Fields proposed in [DolzmannSturm-1997]. In particular, the simplification strategies described under Options.implicit_ranges, Options.lift, and Options.substitute were not part of the original standard simplifier.

logic1.theories.RCF.simplify.simplify(f: Formula, assume: Iterable[AtomicFormula] = [], **options) → Formula[source]#

This is the primary simplification function for f modulo assume. Note that assumptions do not affect bound variables.

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> a, b = VV.get('a', 'b')
>>> simplify(Ex(a, And(a > 5, b > 10)), assume=[a > 10, b > 20])
Ex(a, a - 5 > 0)

See also

Options: for the options recognized by this function.
Simplify: Its inherited method Simplify.is_valid() is wrapped by this function.

class logic1.theories.RCF.simplify.Options[source]#

Bases: Options

Options for Simplify and the functions simplify() and is_valid() based on it. Implements the abstract class abc.simplify.Options.

explode_always: bool = True#

Simplification can split certain atomic formulas built from products or square sums:

Example

\(ab = 0\) is equivalent to \(a = 0 \lor b = 0\)

\(a^2 + b^2 \neq 0\) is equivalent to \(a \neq 0 \lor b \neq 0\)
\(ab \neq 0\) is equivalent to \(a \neq 0 \land b \neq 0\)

\(a^2 + b^2 = 0\) is equivalent to \(a = 0 \land b = 0\)

With explode_always=False the splittings in “1.” are applied only within disjunctions and the ones in “2.” are applied only within conjunctions. This keeps the terms more complex but the Boolean structure simpler.

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> a, b, c = VV.get('a', 'b', 'c')
>>> simplify(And(a * b == 0, c == 0))
And(c == 0, Or(b == 0, a == 0))
>>> simplify(And(a * b == 0, c == 0), explode_always=False)
And(c == 0, a*b == 0)
>>> simplify(Or(a * b == 0, c == 0), explode_always=False)
Or(c == 0, b == 0, a == 0)

implicit_ranges: bool = True#

By default, the simplifier uses explicit numerical bounds on variables, algebraic knowledge like non-negativity of squares, and interval arithmetic to derive bounds on complex terms. Turning this off via implicit_ranges=False reduces the computation time at the price of less simplification.

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> phi = And(10 < x, x < 100, Or(z == 0, And(x*y**2 + x**2 > 0)))
>>> simplify(phi)
And(x - 100 < 0, x - 10 > 0)
>>> simplify(phi, implicit_ranges=False)
And(x - 100 < 0, x - 10 > 0, Or(z == 0, x*y**2 + x**2 > 0))

lift: bool = True#

By default, the simplifier produces atoms with left hand sides that are primitive polynomials over the integers. With lift=False, monic polynomials over the rationals are produced instead.

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> x = VV['x']
>>> phi = 4 * x**2 == 1
>>> simplify(phi)
Or(2*x - 1 == 0, 2*x + 1 == 0)
>>> simplify(phi, lift=False)
Or(x - 1/2 == 0, x + 1/2 == 0)

The name of the option refers to the notion of “lifting” polynomials over the rationals to polynomials over the integers.

prefer_order: bool = True#

One can sometimes equivalently choose between ordering inequalities and disequalities.

Example

\(a > 0 \lor (b = 0 \land a < 0)\) is equivalent to \(a > 0 \lor (b = 0 \land a \neq 0)\)
\(a \geq 0 \land (b = 0 \lor a > 0)\) is equivalent to \(a \geq 0 \land (b = 0 \lor a \neq 0)\)

By default, the left hand sides in the Example are preferred. With prefer_order=False the right hand sides are preferred.

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> a, b = VV.get('a', 'b')
>>> simplify(And(a >= 0, Or(b == 0, a > 0)))
And(a >= 0, Or(b == 0, a > 0))
>>> simplify(And(a >= 0, Or(b == 0, a != 0)))
And(a >= 0, Or(b == 0, a > 0))
>>> simplify(And(a >= 0, Or(b == 0, a > 0)), prefer_order=False)
And(a >= 0, Or(b == 0, a != 0))
>>> simplify(And(a >= 0, Or(b == 0, a != 0)), prefer_order=False)
And(a >= 0, Or(b == 0, a != 0))

The choice depends on the user’s preference and the context. On the one hand, ordering inequalities can be considered more natural than disequalities in algebraic contexts. On the other hand ordering inequalities can be more informative, e.g., when the user is interested in the sign of a term. More generally, they have smaller satisfying sets.

prefer_weak: bool = False#

One can sometimes equivalently choose between strict and weak inequalities.

Example

\(a = 0 \lor (b = 0 \land a \geq 0)\) is equivalent to \(a = 0 \lor (b = 0 \land a > 0)\)
\(a \neq 0 \land (b = 0 \lor a \geq 0)\) is equivalent to \(a \neq 0 \land (b = 0 \lor a > 0)\)

By default, the right hand sides in the Example are preferred. With prefer_weak=True the left hand sides are preferred.

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> a, b = VV.get('a', 'b')
>>> simplify(And(a != 0, Or(b == 0, a >= 0)))
And(a != 0, Or(b == 0, a > 0))
>>> simplify(And(a != 0, Or(b == 0, a > 0)))
And(a != 0, Or(b == 0, a > 0))
>>> simplify(And(a != 0, Or(b == 0, a >= 0)), prefer_weak=True)
And(a != 0, Or(b == 0, a >= 0))
>>> simplify(And(a != 0, Or(b == 0, a > 0)), prefer_weak=True)
And(a != 0, Or(b == 0, a >= 0))

The default has been chosen because strict inequalities are more informative than weak ones, e.g., when the user is interested in the sign of a term. More generally, they have smaller satisfying sets. It is noteworthy that weak inequalities are preferable for the elimination of existential quantifiers via virtual substitution.

substitute: int = 2#

Example

Consider the formula \(\phi\) given by \(d = 2 \land 4b - 3c = 0 \land a + b + c + d \geq 0\).

\(\phi\) is equivalent to \(d = 2 \land 4b - 3c = 0 \land a + b + c + 2 \geq 0\), substituting the value \(d = 2\) wherever adequate.
Going further, \(\phi\) is also equivalent to \(d = 2 \land 4b - 3c = 0 \land 4a + 7c + 8 \geq 0\) additionally substituting the monomial \(b = \frac{3}{4} c\) wherever adequate.

The default is substitute=2, which means that both these simplifications are applied. With substitute=1, only values are substituted. With substitute=0 neither of these simplifications is applied.

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> a, b, c, d = VV.get('a', 'b', 'c', 'd')
>>> phi = And(d == 2, 4*b - 3*c == 0, a + b + c + d >= 0)
>>> simplify(phi, substitute=0)
And(d - 2 == 0, 4*b - 3*c == 0, a + b + c + d >= 0)
>>> simplify(phi, substitute=1)
And(d - 2 == 0, 4*b - 3*c == 0, a + b + c + 2 >= 0)
>>> simplify(phi)
And(d - 2 == 0, 4*b - 3*c == 0, 4*a + 7*c + 8 >= 0)

Lower values of substitute reduce the computation time at the price of less simplification.

Details#

Attention

The material below addresses implementers rather than users.

class logic1.theories.RCF.simplify.Simplify[source]#

Bases: Simplify[AtomicFormula, Term, Variable, int, InternalRepresentation, Options]

Deep simplification following [DolzmannSturm-1997]. Implements the abstract methods create_initial_representation and simpl_at of its super class abc.simplify.Simplify.

The simplifier should be called via the function simplify(). In addition, this class inherits abc.simplify.Simplify.is_valid(), which should be called via the function is_valid().

class logic1.theories.RCF.simplify.InternalRepresentation[source]#

Bases: InternalRepresentation[AtomicFormula, Term, Variable, int]

Implements the abstract methods add(), extract(), and next_() of its super class abc.simplify.InternalRepresentation. Required by RCF.simplify.Simplify for instantiating the type variable abc.simplify.ρ of abc.simplify.Simplify.

Simplification

Contents

Simplification#

Details#