Methods on Formulas#

Data Extraction#

logic1.firstorder.formula.Formula.count_alternations(self) → int

Count number of quantifier alternations.

Returns the maximal number of quantifier alternations along a path in the expression tree. Occurrence of quantified variables is not checked, so that quantifiers with unused variables are counted.

>>> from logic1 import Ex, All, T
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> Ex(x, Eq(x, y) & All(x, Ex(y, Ex(z, T)))).count_alternations()
2

logic1.firstorder.formula.Formula.get_vars(self, assume_quantified: set = {}) → GetVars

Extract all variables occurring in self.

The result is an instance of GetVars, which extract certain subsects of variables as a set.

>>> from logic1 import Ex, All
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> # Variables with free occurrences:
>>> f = Eq(3 * x, 0) >> All(z, All(x,
...     ~ Eq(x, 0) >> Ex(y, Eq(x * y, 1))))
>>> f.get_vars().free == {x}
True
>>>
>>> # Variables with bound occurrences:
>>> f.get_vars().bound == {x, y}
True
>>>
>>> # All occurring variables:
>>> z not in f.get_vars().all
True

Note that following the common definition in logic, occurrence refers to the occurrence in a term. Appearances of variables as a quantified variables without use in any term are not considered. Compare get_qvars().

logic1.firstorder.formula.Formula.get_qvars(self) → set

The set of all variables that are quantified in self.

>>> from logic1 import Ex, All
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import a, b, c, x, y, z
>>>
>>> All(y, Ex(x, Eq(a, y)) & Ex(z, Eq(a, y))).get_qvars() == {x, y, z}
True

Note that the mere quantification of a variable does not establish a bound ocurrence of that variable. Compare get_vars().

Transformations#

logic1.firstorder.formula.Formula.subs(self, substitution: dict) → Self

Substitution of terms for variables.

>>> from logic1 import Ex
>>> from logic1.support import renaming
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import a, b, c, x, y, z
>>> renaming.push()  # temporarily create a fresh counter for renaming
>>>
>>> f = Ex(x, Eq(x, a))
>>> f.subs({x: a})
Ex(x, Eq(x, a))
>>>
>>> f.subs({a: x})
Ex(x_R1, Eq(x_R1, x))
>>>
>>> g = Ex(x, _ & Eq(b, 0))
>>> g.subs({b: x})
Ex(x_R2, And(Ex(x_R1, Eq(x_R1, x_R2)), Eq(x, 0)))
>>>
>>> renaming.pop()  # restore renaming counter

logic1.firstorder.formula.Formula.simplify(self, Theta=None) → Formula

Fast simplification. The result is equivalent to self.

Primary simplification goals are the elimination of occurrences of T and F and of occurrences of equal subformulas as siblings in the expression tree.

logic1.firstorder.formula.Formula.to_latex(self) → str: Convert to a LaTeX representation.

logic1.firstorder.formula.Formula.to_sympy(self, **kwargs) → sympy.core.basic.Basic

Convert to SymPy representation if possible.

Subclasses that have no match in Symy raise NotImplementedError. All keyword arguments are passed on to the SymPy constructors.

>>> from logic1 import Equivalent, T
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y
>>>
>>> e1 = Equivalent(Eq(x, y), Eq(x + 1, y + 1))
>>> type(e1)
<class 'logic1.firstorder.boolean.Equivalent'>
>>>
>>> e1.to_sympy()
Equivalent(Eq(x, y), Eq(x + 1, y + 1))
>>> type(e1.to_sympy())
Equivalent
>>>
>>> e2 = Equivalent(Eq(x, y), Eq(y, x))
>>> e2.to_sympy()
True
>>>
>>> e3 = T
>>> e3.to_sympy()
Traceback (most recent call last):
...
NotImplementedError:
    sympy does not know <class 'logic1.firstorder.truth._T'>
>>>
>>> e4 = All(x, Ex(y, Eq(x, y)))
>>> e4.to_sympy()
Traceback (most recent call last):
...
NotImplementedError:
    sympy does not know <class 'logic1.firstorder.quantified.All'>

logic1.firstorder.formula.Formula.transform_atoms(self, transformation: Callable) → Self

Apply transformation to all atomic formulas.

Replaces each atomic subformula of self with the Formula transformation(self).

>>> from logic1 import And
>>> from logic1.atomlib.sympy import Eq, Lt
>>> from sympy.abc import x, y, z
>>>
>>> f = Eq(x, y) & Lt(y, z)
>>> f.transform_atoms(lambda atom: atom.func(atom.lhs - atom.rhs, 0))
And(Eq(x - y, 0), Lt(y - z, 0))

This often allows to write uniform code for objects where the number or types of elements of args are not known, in particular in recursions.

logic1.firstorder.formula.Formula.to_distinct_vars(self) → Self

Convert to equivalent formulas with distinct variables.

Bound variables are renamed such that that set of all bound variables is disjoint from the set of all free variables. Furthermore, each bound variable in the result occurs with one and only one quantifier.

>>> from logic1 import Ex, All, T
>>> from logic1.support import renaming
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>> renaming.push()  # temporarily create a fresh counter for renaming
>>>
>>> f0 = All(z, Ex(y, Eq(x, y) & Eq(y, z) & Ex(x, T)))
>>> f = Eq(x, y) & Ex(x, Eq(x, y) & f0)
>>> f
And(Eq(x, y), Ex(x, And(Eq(x, y),
    All(z, Ex(y, And(Eq(x, y), Eq(y, z), Ex(x, T)))))))
>>>
>>> f.to_distinct_vars()
And(Eq(x, y), Ex(x_R3, And(Eq(x_R3, y),
    All(z, Ex(y_R2, And(Eq(x_R3, y_R2), Eq(y_R2, z), Ex(x_R1, T)))))))
>>>
>>> renaming.pop()  # restore renaming counter

Normal Forms#

Negation Normal Form#

logic1.firstorder.formula.Formula.to_nnf(self, to_positive: bool = True, _implicit_not: bool = False) → Formula

Convert to Negation Normal Form.

A Negation Normal Form (NNF) is an equivalent formula within which the application of Not is restricted to atomic formulas, i.e., instances of AtomicFormula, and truth values T and F. The only other operators admitted are And, Or, Ex, and All.

If the input is quanitfier-free, to_nnf() will not introduce any quanitfiers.

If to_positive is True, Not is eliminated via replacing relation symbols with their complements. The result is then even a Positive Normal Form.

>>> from logic1 import Ex, Equivalent, T
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import a, y
>>>
>>> f = Equivalent(Eq(a, 0) & T, Ex(y, ~ Eq(y, a)))
>>> f.to_nnf()
And(Or(Ne(a, 0), F, Ex(y, Ne(y, a))),
    Or(All(y, Eq(y, a)), And(Eq(a, 0), T)))

Prenex Normal Form#

Conjunctive and Disjunctive Normal Form#

logic1.firstorder.boolean.BooleanFormula.to_cnf(self) → Formula

Convert to Conjunctive Normal Form.

>>> from logic1.atomlib.sympy import Eq, Ne
>>> from sympy.abc import a
>>>
>>> ((Eq(a, 0) & Ne(a, 1) | ~Eq(a, 0) | Ne(a, 2)) >> Ne(a, 1)).to_cnf()
And(Or(Ne(a, 1), Eq(a, 2)), Or(Eq(a, 0), Ne(a, 1)))

logic1.firstorder.boolean.BooleanFormula.to_dnf(self) → BooleanFormula | AtomicFormula

Convert to Disjunctive Normal Form.

>>> from logic1.atomlib.sympy import Eq, Ne
>>> from sympy.abc import a
>>>
>>> ((Eq(a, 0) & Ne(a, 1) | ~Eq(a, 0) | Ne(a, 2)) >> Ne(a, 1)).to_dnf()
Or(Ne(a, 1), And(Eq(a, 0), Eq(a, 2)))

Methods on Formulas