Redlog Interface

Real Closed Fields

Redlog Interface#

The use of the Redlog interface requires the computer algebra system Reduce. Binary distributions are available on SourceForge. The executable redcsl must be in the system path. Test the following in your shell:

$ redcsl
Reduce (CSL, rev 6864), 24-Aug-2024 ...

1: rlset reals;
Redlog Revision 6618 of 2023-10-06, 06:18:51Z
(c) 1992-2023 T. Sturm and A. Dolzmann (www.redlog.eu)
type ?; for help

{}

2: rlqe ex(x, a*x + b = 0);

b = 0 or a <> 0

3: quit;

This module allows you to perform the same quantifier elimination in Redlog from within Python:

>>> from logic1.interactive.RCF import *
>>> result = redlog.qe(Ex(x, a * x + b == 0))
>>> result
Or(b == 0, a != 0)

Both, the argument of redlog.qe() and the result are instances of Formula.

logic1.theories.RCF.redlog.gqe(f: Formula[AtomicFormula, Term, Variable, int], generic: Generic = Generic.FULL) → tuple[list[AtomicFormula], Formula[AtomicFormula, Term, Variable, int]][source]#

Generic real quantifier elimination using the Redlog function rlgqe.

Parameters:

f – The input formula to which quantifier elimination will be applied.

Returns:

A pair (assumptions, f’). The formula f’ is a quantifier-free equivalent of f modulo the assumptions. All assumptions are instances of Ne; if generic=Generic.MONOMIAL, then all left hand sides of assumptions are monomial .

>>> from logic1 import *
>>> from logic1.theories.RCF import *
>>> a, b, c, x = VV.get('a', 'b', 'c', 'x')
>>> redlog.gqe(Ex(x, (a + 1) * x**2 + b * x + c == 0), generic=Generic.MONOMIAL)
([b != 0], Or(a + 1 == 0, 4*a*c - b**2 + 4*c <= 0))
>>> redlog.gqe(Ex(x, (a + 1) * x**2 + b * x + c == 0), generic=Generic.FULL)
([a + 1 != 0], 4*a*c - b**2 + 4*c <= 0)

See also

logic1.theories.RCF.redlog.qe(f: Formula[AtomicFormula, Term, Variable, int], assume: Iterable[AtomicFormula] = []) → Formula[AtomicFormula, Term, Variable, int][source]#

Real quantifier elimination using the Redlog function rlqe.

Parameters:

  • f – The input formula to which quantifier elimination will be applied.

  • assume – A list of atomic formulas that are assumed to hold. The return value is equivalent modulo those assumptions.

Returns:

A quantifier-free equivalent of f modulo assume.

>>> from logic1 import *
>>> from logic1.theories.RCF import *
>>> a, b, c, x, y = VV.get('a', 'b', 'c', 'x', 'y')
>>> redlog.qe(All(x, Ex(y, x**2 + x*y + b > 0 and x + a*y**2 + b <= 0)));
a < 0
>>> redlog.qe(Ex(x, (a + 1) * x**2 + b * x + c == 0), [b != 0])
Or(a + 1 == 0, 4*a*c - b**2 + 4*c <= 0)
>>> redlog.qe(All(x, Ex(y, And(b + x**2 + x*y > 0, a*y**2 + b + x <= 0))))
And(b > 0, a < 0)

See also

  • The documentation of the Redlog function rlqe.

  • Function qe with the default option generic = Generic.NONE.

logic1.theories.RCF.redlog.qea(f: Formula[AtomicFormula, Term, Variable, int]) → list[tuple[Formula[AtomicFormula, Term, Variable, int], list[str]]][source]#

Extended real quantifier elimination using the Redlog function rlqea.

Parameters:

f – The input formula to which extended quantifier elimination will be applied.

Returns:

A list of pairs (f’, answer). The semantics of the return value depends on quantification of the outermost block of the input formula f:

  • Ex: The disjunction of the guards f’ is equivalent to f. Each answer represents satisfying values of the quantified variables in the corresponding case.

  • All: The conjunction of the guards f’ is equivalent to f. Each answer represents unsatisfying values of the quantified variables in the case that the corresponding f’ does not hold.

>>> from logic1 import *
>>> from logic1.theories.RCF import *
>>> a, b, c, x = VV.get('a', 'b', 'c', 'x')
>>> redlog.qea(Ex(x, a * x**2 + b * x + c == 0))
[(And(c == 0, b == 0, a == 0), ['x = infinity1']),
 (And(a != 0, 4*a*c - b**2 <= 0), ['x = ( - sqrt( - 4*a*c + b**2) - b)/(2*a)']),
 (And(a != 0, 4*a*c - b**2 <= 0), ['x = (sqrt( - 4*a*c + b**2) - b)/(2*a)']),
 (And(b != 0, a == 0), ['x = ( - c)/b'])]

See also

The documentation of the Redlog function rlqea.

logic1.theories.RCF.redlog.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][source]#

Simplification using the Redlog function rlsimpl.

Parameters:

  • f – The input formula to which quantifier elimination will be applied.

  • assume – A list of atomic formulas that are assumed to hold. The return value is equivalent modulo those assumptions.

Returns:

A simplified equivalent of f modulo assume.

See also

The documentation of the Redlog function rlsimpl.