Quantifier Elimination

Real Closed Fields

Quantifier Elimination#

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

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

Real quantifier elimination. Returns a quantifier-free equivalent f' of f modulo the assumptions provided by the attribute qe.assumptions.

\[\textsf{RCF} \models \bigwedge \mathtt{qe.assumptions} \longrightarrow (\mathtt{f} \longleftrightarrow \mathtt{f'}).\]

With regular quantifier elimination, qe.assumptions contains the assumptions passed as the assume parameter, modulo simplification. In particular, we obtain \(\mathbb{R} \models \mathtt{f} \longleftrightarrow \mathtt{f'}\) with the default assume=[]. With generic quantifier elimination [DolzmannSturmWeispfenning-1998], [Sturm-1999], disequalities in the parameters may be added in the course of the elimination.

Technically, logic1.theories.RCF.qe.qe is an instance of the callable class VirtualSubstitution. Its attributes are reset and reused with each call of qe(). Additional, independent instances of quantifier elimination can be created and used as follows:

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> from logic1.theories.RCF.qe import VirtualSubstitution
>>> another_qe = VirtualSubstitution()
>>> a, b, c, x = VV.get('a', 'b', 'c', 'x')
>>> qe(Ex(x, (a + 1) * x**2 + b * x + c == 0), generic=Generic.FULL)
4*a*c - b**2 + 4*c <= 0
>>> another_qe(Ex(x, a * x + b == 0), generic=Generic.FULL)
T
>>> qe.assumptions
[a + 1 != 0]
>>> another_qe.assumptions
[a != 0]

In general, our implementation essentially follows [Kosta-2016] up to degree two. For subproblems in which all terms are weakly parametric linear, we use a specialized approach, which we call Xopt, based on [Weispfenning-1997].

See also

Options: for the options that can be passed to this function. The documentation of the options also contains some more quantifier elimination examples.
Options.generic: explains generic quantifier elimination in more detail.
Options.workers: explains how to specify parallel computation of subproblems.
logic1.theories.RCF.node.Node: The subproblems referred to above correspond to instances of this class.
is_weakly_parametric_linear(): for the definition of “weakly parametric linear terms”.
logic1.theories.RCF.qe.VirtualSubstitution: qe is an instance of this callable class.

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

Bases: Options

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

The options specified here, as well as the options log_level, log_rate, workers inherited from abc.qe.Options, can be passed to qe() as keyword arguments.

clustering: Clustering#

The clustering strategy to be used by qe(). The default is Clustering.FULL. For theoretical details on clustering see [Kosta-2016].

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

>>> phi_6 = Ex(x, And(a * x + b <= 0, x <= b))
>>> qe(phi_6, clustering=Clustering.NONE)
Or(a > 0, And(b <= 0, a == 0), And(a < 0, a*b + b <= 0))
>>> qe(phi_6, clustering=Clustering.FULL)
Or(a > 0, And(b <= 0, a == 0), And(a < 0, a**2*b + a*b >= 0))

>>> phi_7 = Ex(x, a * x**2 + b * x + c == 0)
>>> qe(phi_7, clustering=Clustering.NONE)
Or(And(c == 0, b == 0, a == 0),
   And(b < 0, a == 0), And(b > 0, a == 0),
   And(a < 0, 4*a*c - b**2 == 0), And(a < 0, 4*a*c - b**2 < 0),
   And(a > 0, 4*a*c - b**2 == 0), And(a > 0, 4*a*c - b**2 < 0))
>>> qe(phi_7, clustering=Clustering.FULL)
Or(And(c == 0, b == 0, a == 0),
   And(b != 0, a == 0),
   And(a != 0, 4*a*c - b**2 <= 0))

elimination_order: int#: Strategy for determining the variable elimination order. This option affects only Xopt nodes. With elimination_order=0, variables in each quantifier block are eliminated from the inside out, i.e., the last variable is eliminated first. With elimination_order=1 (default), dynamic heuristics are used to select the next variable to eliminate.

generic: Generic#

The degree of genericity used by the quantifier elimination. The default is Generic.NONE. The principal idea of generic quantifier elimination is to assume certain disequalities on the parameters of the input formula in order to avoid case distinctions during quantifier elimination. Technically, these disequalities are added to qe.assumptions, which is initialized with the assume argument of qe(). The following options are available:

Generic.NONE: uses regular quantifier elimination without making any assumptions.
Generic.MONOMIAL: admits assumptions of the form \(m \neq 0\) where \(m\) is a monomial in the parameters of the input formula.
Generic.FULL: admits assumptions of the form \(p \neq 0\) where \(p\) is a polynomial in the parameters of the input formula.

For theoretical details on generic quantifier elimination see [DolzmannSturmWeispfenning-1998], [Sturm-1999].

>>> 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.MONOMIAL)
Or(a**2 - 2 == 0, 4*a**2*c - b**2 - 8*c <= 0)
>>> qe.assumptions
[c > 0, b != 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]

log_level: int#: The logging level of the logger used

log_rate: float#: The minimal timespan (in s) between log outputs when reporting progress

traditional_guards: bool#

The default is traditional_guards=True. Setting 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))

workers: int#

Controls the number of CPUs used for processing subproblems:

With the default value workers=0, the implementation runs sequentially. For all other values, additional processes are started.
A positive value workers=n uses n + 2 CPUs: n for worker processes that process subproblems, one for the master process, and another one for a proxy process that manages shared data.
A negative value workers=-n uses os.cpu_count() - n CPUs for workers, plus two additional CPUs for the master and proxy processes. It follows that workers=-2 uses all available CPUs, while workers=-3 leaves one CPU free.

Attention

workers=1 uses the parallel implementation with only one worker. Algorithmically, this is similar to the sequential implementation with workers=0, but introduces overhead.
workers=-1 uses os.cpu_count() + 1 CPUs, which is not a natural choice.

Details#

Attention

The material below addresses implementers rather than users.

class logic1.theories.RCF.qe.VirtualSubstitution[source]#

Bases: QuantifierElimination[Node, tuple[Formula[AtomicFormula, Term, Variable, int], frozenset[Term]], 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.

class logic1.theories.RCF.node.Node[source]#

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

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

class logic1.theories.RCF.node.Assumptions[source]#

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.

Quantifier Elimination

Contents

Quantifier Elimination#

Details#