Real Closed Fields

Quantifier Elimination

Real quantifier elimination by virtual substitution [Sturm-2018].

Assumptions

class logic1.theories.RCF.qe.Assumptions

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

Implements the abstract method simplify() of its super class abc.qe.Assumptions. Required by Node and VirtualSubstitution for instantiating the type variable abc.qe.λ of abc.qe.Node and abc.qe.QuantifierElimination, respectively.

Nodes

class logic1.theories.RCF.qe.Node

Bases: Node[Formula[AtomicFormula, Term, Variable, int], Variable, Assumptions]

Implements the abstract methods copy() and process() of its super class abc.qe.Node. Required by VirtualSubstitution for instantiating the type variable abc.qe.ν of abc.qe.QuantifierElimination.

Options

class logic1.theories.RCF.qe.CLUSTERING

Bases: Enum

Available clustering strategies. Required by Options.

NONE = 1

No clustering at all.

FULL = 2

Full clustering.

class logic1.theories.RCF.qe.GENERIC

Bases: Enum

Available degrees of genericity. For details on generic quantifier elimination see

Required by Options.

NONE = 1

Regular quantifier elimination, not making any assumptions.

MONOMIAL = 2

Admit assumptions on parameters by adding atomic formulas to abc.qe.QuantifierElimination.assumptions, where the left hand side of those atomic formulas is a monomial (and the right hand side is zero).

FULL = 3

Admit assumptions on parameters by adding atomic formulas to abc.qe.QuantifierElimination.assumptions.

class logic1.theories.RCF.qe.Options

Bases: Options

The options specified here, as well as the options inherited from abc.qe.Options, can be passed to the callable class VirtualSubstitution as keyword arguments.

Required by VirtualSubstitution for instantiating the type variable abc.qe.ω of abc.qe.QuantifierElimination.

clustering: CLUSTERING = 2

The clustering strategy used by VirtualSubstitution. See [Kosta-2016] for details on clustering.

generic: GENERIC = 1

The degree of genericity used by VirtualSubstitution. See [DolzmannSturmWeispfenning-1998], [Sturm-1999] for details on generic quantifier elimination.

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

>>> qe(Ex(x, (a**2 - 2) * x**2 + b * x + c == 0),
...    assume=[c > 0])
Or(And(b != 0, a^2 - 2 == 0),
   And(a^2 - 2 != 0, 4*a^2*c - b^2 - 8*c <= 0))
>>> qe.assumptions
[c > 0]

>>> qe(Ex(x, (a**2 - 2) * x**2 + b * x + c == 0),
...    assume=[c > 0], generic=GENERIC.FULL)
4*a^2*c - b^2 - 8*c <= 0
>>> qe.assumptions
[c > 0, a^2 - 2 != 0]

>>> qe(Ex(x, (a**2 - 2) * x**2 + b * x + c == 0),
...    assume=[c > 0], generic=GENERIC.MONOMIAL)
Or(a^2 - 2 == 0, 4*a^2*c - b^2 - 8*c <= 0)
>>> qe.assumptions
[c > 0, b != 0]

traditional_guards: bool = True

traditional_guards=False strictly follows the construction of guards as described in [Kosta-2016].

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

>>> qe(Ex(x, a * x**2 + b * x + c == 0))
Or(And(c == 0, b == 0, a == 0),
   And(b != 0, a == 0),
   And(a != 0, 4*a*c - b^2 <= 0))

>>> qe(Ex(x, a * x**2 + b * x + c == 0), traditional_guards=False)
Or(And(c == 0, b == 0, a == 0),
   And(b != 0, Or(c == 0, a == 0)),
   And(a != 0, 4*a*c - b^2 <= 0))

Quantifier Elimination

class logic1.theories.RCF.qe.VirtualSubstitution

Bases: QuantifierElimination[Node, Assumptions, list[str], Options, AtomicFormula, Term, Variable, int]

Real quantifier elimination by virtual substitution.

Implements the abstract methods create_options(), create_root_nodes(), create_assumptions(), create_true_node(), final_simplify(), init_env(), init_env_arg() of its super class abc.qe.QuantifierElimination.

User Interface

logic1.theories.RCF.qe.qe(f: Formula[α, τ, χ, σ], assume: Iterable[α] = [], workers: int = 0, **options) → Formula[α, τ, χ, σ] | None

Real quantifier elimination by virtual substitution. The implementation essentially follows [Kosta-2016] up to degree two. It also offers generic quantifier elimination [DolzmannSturmWeispfenning-1998], [Sturm-1999].

Technically, qe() is an instance of the callable class VirtualSubstitution.

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.

• workers –

  Specifies the number of processes to be used in parallel:

  • The default value workers=0 uses a sequential implementation, which avoids overhead when input problems are small. For all other values, there are additional processes started.

  • A positive value workers=n > 0 uses n + 2 processes: the master process, n worker processes, and a proxy processes that manages shared data.

    Note

    workers=1 uses the parallel implementation with only one worker. Algorithmically this is similar to the sequential version with workers=0 but comes at the cost of 2 additional processes.

  • A negative value workers=-n < 0 specifies os.num_cpu() - n many workers. It follows that workers=-2 exactly allocates all of CPUs of the machine, and workers=-3 is an interesting choice, which leaves one CPU free for smooth interaction with the machine.

• **options – Keyword arguments with keywords corresponding to attributes of Options. Those are clustering, generic, log_level, log_rate, traditional_guards.

Returns:

A quantifier-free equivalent of f modulo assumptions that are available in qe.assumptions at the end of the computation. With regular quantifier elimination, the assumptions are those passed as the assume parameter, modulo simplification. With generic quantifier elimination, inequations in the parameters can be added in the course of the elimination. See Options.generic for examples.