Atomic Formula Library

Atomic Formula Library#

This module provides a library of atomic formulas based on SymPy terms.

class logic1.atomlib.sympy.TermMixin#

Bases: object

static term_type() → type[sympy.core.expr.Expr]#: Implements the abstract method firstorder.AtomicFormula.term_type().

static term_get_vars(term: Expr) → set[sympy.core.symbol.Symbol]#: Implements the abstract method firstorder.AtomicFormula.term_get_vars().

static term_to_latex(term: Expr) → str#: Implements the abstract method firstorder.AtomicFormula.term_to_latex().

static term_to_sympy(term: Expr) → Basic#: Implements the abstract method firstorder.AtomicFormula.term_to_sympy().

static variable_type() → type[sympy.core.symbol.Symbol]#: Implements the abstract method firstorder.AtomicFormula.variable_type().

static rename_var(variable: Symbol) → Symbol#: Implements the abstract method firstorder.AtomicFormula.rename_var().

class logic1.atomlib.sympy.AtomicFormula(*args)#

Bases: TermMixin, AtomicFormula

Atomic Formula with Sympy Terms. All terms are sympy.Expr.

get_vars(assume_quantified: set = {}) → GetVars#: Implements the abstract method firstorder.Formula.get_vars().

subs(substitution: dict) → AtomicFormula#: Implements the abstract method firstorder.Formula.subs().

class logic1.atomlib.sympy.BinaryAtomicFormula(*args)#

Bases: AtomicFormula

A class whose instances are binary formulas in the sense that both their m-arity and their p-arity is 2.

Let R be a subclass of BinaryAtomicFormula implementing atomic formulas with a binary relation symbol \(r\). For instance, if R is Eq, then \(r\) stands for the equality relation \(=\) in the following discussion:

>>> Eq(0, 0).func
<class 'logic1.atomlib.sympy.Eq'>
>>> Eq.func
<class 'logic1.atomlib.sympy.Eq'>

Assume that \(r\) is defined on a domain \(D\). Then the complement relation of \(r\) is defined as \(\overline{r} = D^2 \setminus r\). It is avaialable as a class property R.complement_func, e.g.:

>>> rels = (Eq, Ne, Ge, Le, Gt, Lt)
>>> tuple(r.complement_func for r in rels)
(<class 'logic1.atomlib.sympy.Ne'>,
 <class 'logic1.atomlib.sympy.Eq'>,
 <class 'logic1.atomlib.sympy.Lt'>,
 <class 'logic1.atomlib.sympy.Gt'>,
 <class 'logic1.atomlib.sympy.Le'>,
 <class 'logic1.atomlib.sympy.Ge'>)

Since \(\overline{r}(s, t)\) is equivalent to \(\neg r(s, t)\), the availability of complement relations is relevant for the computation of positive negation normal forms; compare firstorder.Formula.to_nnf() with keyword argument to_positive=True.

The converse relation of \(r\) is defined as \(r^{-1} = \{ (x, y) \in D : (y, x) \in r \}\). It is avaialable as a class property R.converse_func, e.g.:

>>> tuple(r.converse_func for r in rels)
(<class 'logic1.atomlib.sympy.Eq'>,
 <class 'logic1.atomlib.sympy.Ne'>,
 <class 'logic1.atomlib.sympy.Le'>,
 <class 'logic1.atomlib.sympy.Ge'>,
 <class 'logic1.atomlib.sympy.Lt'>,
 <class 'logic1.atomlib.sympy.Gt'>)

The converse relation is the inverse with respect to composition.

Finally, the dual relation of \(r\) is defined as \(\overline{r}^{-1}\). It is available as a class property R.dual_func. Generally, \(\overline{r}^{-1} = \overline{r^{-1}}\), e.g.:

>>> tuple(r.dual_func for r in rels)
(<class 'logic1.atomlib.sympy.Ne'>,
 <class 'logic1.atomlib.sympy.Eq'>,
 <class 'logic1.atomlib.sympy.Gt'>,
 <class 'logic1.atomlib.sympy.Lt'>,
 <class 'logic1.atomlib.sympy.Ge'>,
 <class 'logic1.atomlib.sympy.Le'>)
>>> all(r.dual_func == r.complement_func.converse_func for r in rels)
True
>>> all(r.dual_func == r.converse_func.complement_func for r in rels)
True

In the context of orderings, dualization turns strict inequalities into weak inequalities, and vice versa. Note that we also have duality and corresponding properties with Boolean functions, which is defined differently.

All those operators on relations are involutive:

>>> all(r.complement_func.complement_func == r for r in rels)
True
>>> all(r.converse_func.converse_func == r for r in rels)
True
>>> all(r.dual_func.dual_func == r for r in rels)
True

class property dual_func#

A class property yielding the dual class of this class or of the derived subclass.

There is an implicit assumption that there are abstract class properties complement_func and converse_func specified, which is technically not possible at the moment.

property lhs: Expr#: The left-hand side of the BinaryAtomicFormula.

property rhs: Expr#: The right-hand side of the BinaryAtomicFormula.

class logic1.atomlib.sympy.Eq(*args)#

Bases: BinaryAtomicFormula

A class whose instances are equations in the sense that their toplevel operator represents the relation symbol \(=\).

>>> from sympy import exp, I, pi
>>> from sympy.abc import t
>>>
>>> equation = Eq(exp(t * I * pi, evaluate=False), -1)
>>> equation
Eq(exp(I*pi*t), -1)
>>> equation.lhs
exp(I*pi*t)
>>> equation.rhs
-1

class property complement_func#: A class property yielding the complement class Ne of Eq.

class property converse_func#: A class property yielding the converse class Eq of Eq.

latex_symbol: str = '='#

A class variable holding a LaTeX symbol for Eq.

This is used with firstorder.Formula.to_latex(), which is in turn used for the output in Jupyter notebooks.

text_symbol: str = '=='#

A class variable holding a representation of Eq suitable for string representation.

This is used for string conversions, e.g., explicitly with the constructor of str or implicitly with print().

simplify(Theta=None)#

Compare the parent method firstorder.Formula.simplify().

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

class logic1.atomlib.sympy.Ne(*args)#

Bases: BinaryAtomicFormula

A class whose instances are inequations in the sense that their toplevel operator represents the relation symbol \(\neq\).

>>> Ne(1, 0)
Ne(1, 0)

class property complement_func#: A class property yielding the complement class Eq of Ne.

class property converse_func#: A class property yielding the converse class Ne of Ne.

latex_symbol: str = '\\neq'#

A class variable holding a LaTeX symbol for Ne.

This is used with firstorder.Formula.to_latex(), which is in turn used for the output in Jupyter notebooks.

text_symbol: str = '!='#

A class variable holding a representation of Ne suitable for string representation.

This is used for string conversions, e.g., explicitly with the constructor of str or implicitly with print().

simplify(Theta=None)#

Compare the parent method firstorder.Formula.simplify().

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

class logic1.atomlib.sympy.Ge(*args)#

Bases: BinaryAtomicFormula

A class whose instances are inequalities where the toplevel operator represents the relation symbol \(\geq\).

>>> Ge(1, 0)
Ge(1, 0)

class property complement_func#: A class property yielding the complement class Lt of Ge.

class property converse_func#: A class property yielding the converse class Le of Ge.

latex_symbol: str = '\\geq'#

A class variable holding a LaTeX symbol for Ge.

This is used with firstorder.Formula.to_latex(), which is in turn used for the output in Jupyter notebooks.

text_symbol: str = '>='#

A class variable holding a representation of Ge suitable for string representation.

This is used for string conversions, e.g., explicitly with the constructor of str or implicitly with print().

class logic1.atomlib.sympy.Le(*args)#

Bases: BinaryAtomicFormula

A class whose instances are inequalities where the toplevel operator represents the relation symbol \(\leq\).

>>> Le(1, 0)
Le(1, 0)

class property complement_func#: A class property yielding the complement class Gt of Le.

class property converse_func#: A class property yielding the converse class Ge of Le.

latex_symbol: str = '\\leq'#

A class variable holding a LaTeX symbol for Le.

This is used with firstorder.Formula.to_latex(), which is in turn used for the output in Jupyter notebooks.

text_symbol: str = '<='#

A class variable holding a representation of Le suitable for string representation.

This is used for string conversions, e.g., explicitly with the constructor of str or implicitly with print().

class logic1.atomlib.sympy.Gt(*args)#

Bases: BinaryAtomicFormula

A class whose instances are inequalities where the toplevel operator represents the relation symbol \(>\).

>>> Gt(1, 0)
Gt(1, 0)

class property complement_func#: A class property yielding the complement class Le of Gt.

class property converse_func#: A class property yielding the converse class Lt of Gt.

latex_symbol: str = '>'#

A class variable holding a LaTeX symbol for Gt.

This is used with firstorder.Formula.to_latex(), which is in turn used for the output in Jupyter notebooks.

text_symbol: str = '>'#

A class variable holding a representation of Gt suitable for string representation.

This is used for string conversions, e.g., explicitly with the constructor of str or implicitly with print().

class logic1.atomlib.sympy.Lt(*args)#

Bases: BinaryAtomicFormula

A class whose instances are inequalities where the toplevel operator represents the relation symbol \(<\).

>>> Lt(1, 0)
Lt(1, 0)

class property complement_func#: A class property yielding the complement class Ge of Lt.

class property converse_func#: A class property yielding the converse class Gt of Lt.

latex_symbol: str = '<'#

A class variable holding a LaTeX symbol for Lt.

This is used with firstorder.Formula.to_latex(), which is in turn used for the output in Jupyter notebooks.

text_symbol: str = '<'#

A class variable holding a representation of Lt suitable for string representation.

This is used for string conversions, e.g., explicitly with the constructor of str or implicitly with print().

class logic1.atomlib.sympy.IndexedConstantAtomicFormula(*args)#

Bases: AtomicFormula

A class whose instances form a family of atomic formulas with m-arity 0. Their p-arity is 1, where the one argument of the constructor is the index.

property index: Any#: The index of the IndexedConstantAtomicFormula.

get_vars(assume_quantified: set = {}) → GetVars#: Implements the abstract method firstorder.Formula.get_vars().

class logic1.atomlib.sympy.C(*args)#

Bases: IndexedConstantAtomicFormula

A class whose instances are cardinality constraints in the sense that their toplevel operator represents a constant relation symbol \(C_n\) where \(n \in \mathbb{N} \cup \{\infty\}\). A typical interpretation in a domain \(D\) is that \(C_n\) holds iff \(|D| \geq n\).

The class constructor takes one argument, which is the index n. It takes care that instance with equal indices are identical.

>>> c_0_1 = C(0)
>>> c_0_2 = C(0)
>>> c_oo = C(oo)
>>> c_0_1 is c_0_2
True
>>> c_0_1 == c_oo
False

class property complement_func#: A class property yielding the complement class C_ of C.

class logic1.atomlib.sympy.C_(*args)#

Bases: IndexedConstantAtomicFormula

A class whose instances are cardinality constraints in the sense that their toplevel operator represents a constant relation symbol \(\bar{C}_n\) where \(n \in \mathbb{N} \cup \{\infty\}\). A typical interpretation in a domain \(D\) is that \(\bar{C}_n\) holds iff \(|D| < n\).

The class constructor takes one argument, which is the index n. It takes care that instance with equal indices are identical.

>>> c_0_1 = C_(0)
>>> c_0_2 = C_(0)
>>> c_oo = C_(oo)
>>> c_0_1 is c_0_2
True
>>> c_0_1 == c_oo
False

class property complement_func#: A class property yielding the complement class C of C_.

Atomic Formula Library

Contents

Atomic Formula Library#