Real Closed Fields

Simplification

This module provides an implementation of deep simplifcication based on generating and propagating internal representations during recursion in Real Closed fields. This is essentially the standard simplifier, which has been proposed for Ordered Fields in [DolzmannSturm-1997].

Internal Representations

class logic1.theories.RCF.simplify.InternalRepresentation

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

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

Simplification and Validity

class logic1.theories.RCF.simplify.Simplify

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

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 simplify(), as described below. In addition, this class inherits abc.simplify.Simplify.is_valid(), which should be called via is_valid(), as described below.

User Interface

logic1.theories.RCF.simplify.simplify(f: Formula[AtomicFormula, Term, Variable, int], assume: Iterable[AtomicFormula] = [], explode_always: bool = True, prefer_order: bool = True, prefer_weak: bool = False) → Formula[AtomicFormula, Term, Variable, int]

Simplify f modulo assume.

Parameters:

• f – The formula to be simplified

• assume –

  A list of atomic formulas that are assumed to hold. The simplification result is equivalent modulo those assumptions. 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)
  

• explode_always –

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

  Example

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

     2. \(a^2 + b^2 \neq 0\) is equivalent to \(a \neq 0 \lor b \neq 0\);

  2. 1. \(ab \neq 0\) is equivalent to \(a \neq 0 \land b \neq 0\)

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

  If explode_always is False, the splittings in “1.” are only applied within disjunctions and the ones in “2.” are only applied within conjunctions. This keeps 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)
  

• prefer_order –

  One can sometimes equivalently choose between order inequalities and (in)equations.

  Example

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

  2. \(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. If prefer_order is False, then 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))
  

• prefer_weak –

  One can sometimes equivalently choose between strict and weak inequalities.

  Example

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

  2. \(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. If prefer_weak is True, then 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))
  

Returns:

A simplified equivalent of f modulo assume.

logic1.theories.RCF.simplify.is_valid(f: Formula[α, τ, χ, σ], assume: Iterable[α] = []) → bool | None

Simplification-based heuristic test for vailidity of a formula.

Mathematical definition

A first-order formula is valid if it holds for all values all free variables.

Parameters:

• f – The formula to be tested for validity

• assume – A list of atomic formulas that are assumed to hold. The result of the validity test is correct modulo these assumptions.

Returns:

Returns True or False if abc.simplify.Simplify.simplify() succeeds in heuristically simplifying f to T or F, respectively. Returns None in the sense of “don’t know” otherwise.

Some examples

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> a, b, c = VV.get('a', 'b', 'c')

>>> is_valid(3 * b**2 + c**2 >= 0)
True

>>> is_valid(3 * b**2 + c**2 < 0)
False

In our last example, validity holds, but the simplifier is not strong enough to deduce T:

>>> is_valid(a * b**2 + c**2 >= 0, assume=[a > 0])  # returns None