Package logic1.theories

Module sets

logic1.theories.sets.show_progress(flag: bool = True) → None

class logic1.theories.sets.TermMixin

Bases: object

static term_type() → type[sympy.core.symbol.Symbol]

static variable_type() → type[sympy.core.symbol.Symbol]

class logic1.theories.sets.Eq(*args)

Bases: TermMixin, Eq

Equations with only variables as terms.

This implements that fact that the language of sets has no functions and, in particular, no constants.

>>> from sympy.abc import x, y
>>> Eq(x, y)
Eq(x, y)

>>> Eq(x, 0)
Traceback (most recent call last):
...
ValueError: 0 is not a Term

>>> Eq(x + x, y)
Traceback (most recent call last):
...
ValueError: 2*x is not a Term

converse_func

alias of Eq

class logic1.theories.sets.Ne(*args)

Bases: TermMixin, Ne

Inequations with only variables as terms.

This implements that fact that the language of sets has no functions and, in particular, no constants.

>>> from sympy.abc import x, y
>>> Ne(y, x)
Ne(y, x)

>>> Ne(x, y + 1)
Traceback (most recent call last):
...
ValueError: y + 1 is not a Term

converse_func

alias of Ne

class logic1.theories.sets.C(*args)

Bases: C

class logic1.theories.sets.C_(*args)

Bases: C_

class logic1.theories.sets.QuantifierElimination(blocks=None, matrix=None, negated=None, pool=None, finished=None)

Bases: QuantifierElimination

Quantifier elimination for the theory of Sets.

>>> from logic1 import *
>>> from sympy.abc import a, u, v, w, x, y, z
>>> f = All(u, Ex(w, All(x, Ex(y, Ex(v, (Eq(u, v) | Ne(v, w))
...     & ~ Equivalent(Eq(u, x), Ne(u, w)) & Eq(y, a))))))
>>> qe(f)
C_(2)

>>> g = Ex(x, Ex(y, Ex(z, Ne(x, y) & Ne(x, z) & Ne(y, z)
...     & All(u, Eq(u, x) | Eq(u, y) | Eq(u, z)))))
>>> qe(g)
And(C(2), C(3), C_(4))

>>> h = Ex(w, Ex(x, Ne(w, x))) >> Ex(w, Ex(x, Ex(y, Ex(z,
...     Ne(w, x) & Ne(w, y) & Ne(w, z) & Ne(x, y) & Ne(x, z) & Ne(y, z)))))
>>> qe(h)
Or(And(C(2), C(3), C(4)), C_(2))

qe1p(v: Symbol, f: Formula) → Formula

static is_valid_atom(f: Formula) → bool