Sets with Cardinality Constraints

Quantifier Elimination

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

Quantifier elimination for the theory of sets with cardinanity constraints. Returns a quantifier-free equivalent f' of f modulo the assumptions passed in the assume parameter.

\[\textsf{Sets} \models \bigwedge \mathtt{assume} \longrightarrow (\mathtt{f} \longleftrightarrow \mathtt{f'}).\]

See also

logic1.abc.qe.Options

for the options that can be passed to this function.

logic1.abc.qe.Options.workers

explains how to specify parallel computation of subproblems.

logic1.theories.Sets.qe.Node

The subproblems referred to above correspond to instances of this class.

logic1.theories.Sets.qe.QuantifierElimination

qe is an instance of this callable class.

Some examples

>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> a, u, v, w, x, y, z = VV.get('a', 'u', 'v', 'w', 'x', 'y', 'z')

For the following input formula to hold, there must be at least two different elements in the universe. We derive this information via quantifier elimination:

>>> qe(Ex([x, y], x != y))
C(2)

See also

The documentation of C and C_.

In the next example, we learn that there must be at most one element in the universe:

>>> qe(All(u, Ex(w, All(x, Ex([y, v],
...   And(Or(u == v, v != w), ~ Equivalent(u == x, u != w), y == a))))))
C_(2)

In the next example, the cardinality of the universe must be exactly three:

>>> qe(Ex([x, y, z],
...   And(x != y, x != z, y != z, All(u, Or(u == x, u == y, u == z)))))
And(C(3), C_(4))

In our final example, the cardinality of the universe must be exactly one or at least 4:

>>> qe(Implies(Ex([w, x], w != x),
...            Ex([w, x, y, z],
...              And(w != x, w != y, w != z, x != y, x != z, y != z))))
Or(C_(2), C(4))

Details

Attention

The material below addresses implementers rather than users.

class logic1.theories.Sets.qe.QuantifierElimination

Bases: QuantifierElimination[Node, Formula[AtomicFormula, Variable, Variable, Never], Assumptions, None, Options, AtomicFormula, Variable, Variable, Never]

Quantifier elimination for the theory of sets with cardinality constraints.

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.Sets.qe.Node

Bases: Node[AtomicFormula, Variable, Variable, Never, Assumptions, Formula[AtomicFormula, Variable, Variable, Never]]

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

class logic1.theories.Sets.qe.Assumptions

Bases: Assumptions[AtomicFormula, Variable, Variable, Never]

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