First-order Formulas

A package providing first-order formulas.

This package provides first-order formulas as a class Formula to the outside world. Technically, Formula is an abstract base class with a hierarchy of subclasses underneath.

Amnong those subclasses, there are subclasses Ex, All, Equivalent, Implies, And, Or, Not, _T, and _F for constructing subformulas with the respective toplevel operator.

Furthermore, there is another abstract base class AtomicFormula, from which modules outside logic1.firstorder derive classes that implement selections of atomic formulas with certain relation symbols as their toplevel operators. The package logic1.firstorder itself makes no assumptions on admissible relation symbols and function symbols, or on the representation of atomic formulas and terms. Of course, the abstract methods specified by AtomicFormula must be implemented.

class logic1.firstorder.Formula(*args)

Bases: ABC

An abstract base class for first-order formulas.

All other classes in the firstorder package are derived from Formula.

final __and__(other: Formula) → Formula

Override the & operator to apply And.

>>> from logic1.atomlib.sympy import Eq
>>>
>>> Eq(0, 0) & Eq(1 + 1, 2) & Eq(1 + 1 + 1, 3)
And(Eq(0, 0), Eq(2, 2), Eq(3, 3))

final __invert__() → Formula

Override the ~ operator to apply Not.

>>> from logic1.atomlib.sympy import Eq
>>>
>>> ~ Eq(1,0)
Not(Eq(1, 0))

final __lshift__(other: Formula) → Formula

Override the << operator to apply Implies with reversed sides.

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> Eq(x + z, y + z) << Eq(x, y)
Implies(Eq(x, y), Eq(x + z, y + z))

final __or__(other: Formula) → Formula

Override the | operator to apply Or.

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> Eq(x, 0) | Eq(x, y) | Eq(x, z)
Or(Eq(x, 0), Eq(x, y), Eq(x, z))

final __rshift__(other: Formula) → Formula

Override the >> operator to apply Implies.

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> Eq(x, y) >> Eq(x + z, y + z)
Implies(Eq(x, y), Eq(x + z, y + z))

final count_alternations() → 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

abstract get_any_atom() → AtomicFormula | None

Return any atomic formula contained in self, or None if there is none.

A typical use case is getting access to static methods of classes derived from atomic.AtomicFormula elsewhere.

>>> from logic1 import Ex, And
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> f = Ex(x, Eq(x, -y) & Eq(y, z ** 2))
>>> isinstance(f.var, f.get_any_atom().variable_type())
True

abstract get_qvars() → 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().

abstract get_vars(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().

simplify(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.

abstract subs(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

final to_distinct_vars() → 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

final to_latex() → str

Convert to a LaTeX representation.

abstract to_nnf(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)))

final to_pnf(prefer_universal: bool = False, is_nnf: bool = False) → Formula

Convert to Prenex Normal Form.

A Prenex Normal Form (PNF) is a Negation Normal Form (NNF) in which all quantifiers Ex and All stand at the beginning of the formula. The method used here minimizes the number of quantifier alternations in the prenex block [Burhenne90].

If the minimal number of alternations in the result can be achieved with both Ex and All as the first quantifier in the result, then the former is preferred. This preference can be changed with a keyword argument prefer_universal=True.

An keyword argument is_nnf=True indicates that self is already in NNF. to_pnf() then skips the initial NNF computation, which can be useful in time-critical situations.

Example from p.88 in [Burhenne90]:

>>> from logic1 import Ex, All, T, F
>>> from logic1.support import renaming
>>> from logic1.atomlib.sympy import Eq
>>> import sympy
>>>
>>> renaming.push()  # temporarily create a fresh counter for renaming
>>> x = sympy.symbols('x:8')
>>> f1 = Ex(x[1], All(x[2], All(x[3], T)))
>>> f2 = All(x[4], Ex(x[5], All(x[6], F)))
>>> f3 = Ex(x[7], Eq(x[0], 0))
>>> (f1 & f2 & f3).to_pnf()
All(x4, Ex(x1, Ex(x5, Ex(x7, All(x2, All(x3, All(x6,
    And(T, F, Eq(x0, 0)))))))))
>>> renaming.pop()  # restore renaming counter

Derived from the rlpnf test in redlog.tst:

>>> from logic1 import Ex, All, Equivalent, And, Or
>>> from logic1.support import renaming
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import a, b, y
>>>
>>> renaming.push()
>>> f1 = Eq(a, 0) & Eq(b, 0) & Eq(y, 0)
>>> f2 = Ex(y, Eq(y, a) | Eq(a, 0))
>>> Equivalent(f1, f2).to_pnf()
Ex(y_R1, All(y_R2,
    And(Or(Ne(a, 0), Ne(b, 0), Ne(y, 0), Eq(y_R1, a), Eq(a, 0)),
        Or(And(Ne(y_R2, a), Ne(a, 0)),
           And(Eq(a, 0), Eq(b, 0), Eq(y, 0))))))
>>> renaming.pop()
>>>
>>> renaming.push()
>>> Equivalent(f1, f2).to_pnf(prefer_universal=True)
All(y_R2, Ex(y_R1,
    And(Or(Ne(a, 0), Ne(b, 0), Ne(y, 0), Eq(y_R1, a), Eq(a, 0)),
        Or(And(Ne(y_R2, a), Ne(a, 0)),
           And(Eq(a, 0), Eq(b, 0), Eq(y, 0))))))
>>> renaming.pop()

[Burhenne90] (1,2)

Klaus-Dieter Burhenne. Implementierung eines Algorithmus zur Quantorenelimination für lineare reelle Probleme. Diploma Thesis, University of Passau, Germany, 1990

to_sympy(**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'>

abstract transform_atoms(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))

class logic1.firstorder.QuantifiedFormula(variable: Any, arg: Formula)

Bases: Formula

A class whose instances are quanitfied formulas in the sense that their toplevel operator is a one of the quantifiers \(\exists\) or \(\forall\).

Note that members of QuantifiedFormula may have subformulas with other logical operators deeper in the expression tree.

latex_symbol_spacing = ' \\, '

A class variable holding LaTeX spacing that comes after a quantifier symbol and its quantified variable.

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

text_symbol_spacing = ' '

A class variable holding spacing that comes after a quantifier symbol and its quantified variable in string representation.

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

print_precedence = 99

A class variable holding the precedence of the operators of instances of QuantifiedFormula in LaTeX and string conversions.

This is compared with the corresponding print_precedence of other classes for placing parentheses.

property var: Any

The variable of the quantifier.

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y
>>>
>>> e1 = All(x, Ex(y, Eq(x, y)))
>>> e1.var
x

property arg: Formula

The subformula in the scope of the QuantifiedFormula.

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y
>>>
>>> e1 = All(x, Ex(y, Eq(x, y)))
>>> e1.arg
Ex(y, Eq(x, y))

get_any_atom() → AtomicFormula | None

Implements the abstract method Formula.get_any_atom().

get_qvars() → set

Implements the abstract method Formula.get_qvars().

get_vars(assume_quantified: set = {}) → GetVars

Implements the abstract method Formula.get_vars().

simplify(Theta=None) → Formula

Compare the parent method Formula.simplify().

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y
>>>
>>> All(x, Ex(y, Eq(x, y))).simplify()
All(x, Ex(y, Eq(x, y)))

subs(substitution: dict) → QuantifiedFormula

Implements the abstract method Formula.subs().

to_nnf(to_positive: bool = True, _implicit_not: bool = False) → Formula

Implements the abstract method Formula.to_nnf().

to_sympy(*args, **kwargs)

Raises NotImplementedError since SymPy does not know quantifiers.

transform_atoms(transformation: Callable) → QuantifiedFormula

Implements the abstract method Formula.transform_atoms().

class logic1.firstorder.Ex(variable: Any, arg: Formula)

Bases: QuantifiedFormula

A class whose instances are existentially quanitfied formulas in the sense that their toplevel operator represents the quantifier symbol \(\exists\).

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x
>>>
>>> Ex(x, Eq(x, 1))
Ex(x, Eq(x, 1))

class property func

A class property yielding the class Ex itself.

class property dual_func

A class property yielding the dual class All of Ex.

latex_symbol: str = '\\exists'

A class variable holding a LaTeX symbol for Ex.

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

text_symbol: str = 'Ex'

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

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

class logic1.firstorder.All(variable: Any, arg: Formula)

Bases: QuantifiedFormula

A class whose instances are universally quanitfied formulas in the sense that their toplevel operator represents the quantifier symbol \(\forall\).

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y
>>>
>>> All(x, All(y, Eq((x + y)**2 + 1, x**2 + 2*x*y + y**2)))
All(x, All(y, Eq((x + y)**2 + 1, x**2 + 2*x*y + y**2)))

class property func

A class property yielding the class All itself.

class property dual_func

A class property yielding the dual class Ex of All.

latex_symbol: str = '\\forall'

A class variable holding a LaTeX symbol for All.

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

text_symbol: str = 'All'

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

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

class logic1.firstorder.BooleanFormula(*args)

Bases: Formula

A class whose instances are Boolean formulas in the sense that their toplevel operator is one of the Boolean operators \(\lnot\), \(\wedge\), \(\vee\), \(\longrightarrow\), \(\longleftrightarrow\).

Note that members of BooleanFormula may have subformulas with other logical operators deeper in the expression tree.

latex_symbol_spacing = ' \\, '

A class variable holding LaTeX spacing that comes after prefix operators and around infix operators.

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

text_symbol_spacing = ' '

A class variable holding spacing that comes after prefix operators and around infix operators in string representation.

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

get_any_atom() → AtomicFormula | None

Implements the abstract method Formula.get_any_atom().

get_qvars() → set

Implements the abstract method Formula.get_qvars().

get_vars(assume_quantified: set = {}) → GetVars

Implements the abstract method Formula.get_vars().

subs(substitution: dict) → BooleanFormula

Implements the abstract method Formula.subs().

to_cnf() → 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)))

to_dnf() → 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)))

transform_atoms(transformation: Callable) → BooleanFormula

Implements the abstract method Formula.transform_atoms().

class logic1.firstorder.Equivalent(lhs: Formula, rhs: Formula)

Bases: BooleanFormula

A class whose instances are equivalences in the sense that their toplevel operator represents the Boolean operator \(\longleftrightarrow\).

class property func

A class property yielding the class Equivalent itself.

latex_symbol: str = '\\longleftrightarrow'

A class variable holding a LaTeX symbol for Equivalent.

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

text_symbol: str = '<-->'

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

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

print_precedence = 10

A class variable holding the precedence of latex_symbol and text_symbol in LaTeX and string conversions.

This is compared with the corresponding print_precedence of other classes for placing parentheses.

print_style: str = 'infix'

A class variable indicating the use of of latex_symbol and text_symbol as an infix operators in LaTeX and string conversions.

property lhs: Formula

The left-hand side of the equivalence.

property rhs: Formula

The right-hand side of the equivalence.

simplify(Theta=None) → Formula

Compare the parent method Formula.simplify().

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y
>>>
>>> e1 = Equivalent(~ Eq(x, y), F)
>>> e1.simplify()
Eq(x, y)

to_nnf(to_positive: bool = True, _implicit_not: bool = False) → BooleanFormula | AtomicFormula

Implements the abstract method Formula.to_nnf().

class logic1.firstorder.Implies(lhs: Formula, rhs: Formula)

Bases: BooleanFormula

A class whose instances are equivalences in the sense that their toplevel operator represents the Boolean operator \(\longrightarrow\).

class property func

A class property yielding the class Implies itself.

latex_symbol: str = '\\longrightarrow'

A class variable holding a LaTeX symbol for Implies.

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

text_symbol: str = '-->'

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

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

print_precedence = 10

A class variable holding the precedence of latex_symbol and text_symbol in LaTeX and string conversions.

This is compared with the corresponding print_precedence of other classes for placing parentheses.

print_style: str = 'infix'

A class variable indicating the use of of latex_symbol and text_symbol as an infix operators in LaTeX and string conversions.

property lhs: Formula

The left-hand side of the implication.

property rhs: Formula

The right-hand side of the implication.

simplify(Theta=None) → Formula

Compare the parent method Formula.simplify().

to_nnf(to_positive: bool = True, _implicit_not: bool = False) → BooleanFormula | AtomicFormula

Implements the abstract method Formula.to_nnf().

class logic1.firstorder.AndOr(*args)

Bases: BooleanFormula

print_precedence = 50

A class variable holding the precedence of the operators of instances of AndOr in LaTeX and string conversions.

This is compared with the corresponding print_precedence of other classes for placing parentheses.

print_style: str = 'infix'

A class variable indicating the use of operators of instances of AndOr as infix in LaTeX and string conversions.

simplify(Theta=None)

Compare the parent method Formula.simplify().

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> f1 = And(Eq(x, y), T, Eq(x, y), And(Eq(x, z), Eq(x, x + z)))
>>> f1.simplify()
And(Eq(x, y), Eq(x, z), Eq(x, x + z))
>>>
>>> f2 = Or(Eq(x, 0), Or(Eq(x, 1), Eq(x, 2)), And(Eq(x, y), Eq(x, z)))
>>> f2.simplify()
Or(Eq(x, 0), Eq(x, 1), Eq(x, 2), And(Eq(x, y), Eq(x, z)))

to_nnf(to_positive: bool = True, _implicit_not: bool = False) → AndOr

Implements the abstract method Formula.to_nnf().

class logic1.firstorder.And(*args, flatten: bool = True)

Bases: AndOr

A class whose instances are conjunctions in the sense that their toplevel operator represents the Boolean operator \(\wedge\).

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> And()
T
>>>
>>> And(Eq(0, 0))
Eq(0, 0)
>>>
>>> And(Eq(x, 0), Eq(x, y), Eq(y, z))
And(Eq(x, 0), Eq(x, y), Eq(y, z))

class property func

A class property yielding the class And itself.

class property dual_func

A class property yielding the class Or, which implements the dual operator \(\lor\) or \(\land\).

latex_symbol: str = '\\wedge'

A class variable holding a LaTeX symbol for And.

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

text_symbol: str = '&'

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

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

class logic1.firstorder.Or(*args, flatten: bool = True)

Bases: AndOr

A class whose instances are disjunctions in the sense that their toplevel operator represents the Boolean operator \(\vee\).

>>> from logic1.atomlib.sympy import Eq
>>>
>>> Or()
F
>>>
>>> Or(Eq(1, 0))
Eq(1, 0)
>>>
>>> Or(Eq(1, 0), Eq(2, 0), Eq(3, 0))
Or(Eq(1, 0), Eq(2, 0), Eq(3, 0))

class property func

A class property yielding the class Or itself.

class property dual_func

A class property yielding the class And, which implements the dual operator \(\land\) or \(\lor\).

latex_symbol: str = '\\vee'

A class variable holding a LaTeX symbol for Or.

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

text_symbol: str = '|'

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

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

class logic1.firstorder.Not(arg: Formula)

Bases: BooleanFormula

A class whose instances are negated formulas in the sense that their toplevel operator is the Boolean operator \(\neg\).

class property func

A class property yielding the class Not itself.

latex_symbol: str = '\\neg'

A class variable holding a LaTeX symbol for Not.

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

text_symbol: str = '~'

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

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

print_precedence = 99

A class variable holding the precedence of the operators of instances of Not in LaTeX and string conversions.

This is compared with the corresponding print_precedence of other classes for placing parentheses.

print_style: str = 'not'

A class variable indicating the use of operators of instances of Not as prefix in LaTeX and string conversions.

property arg: Formula

The one argument of the operator \(\neg\).

simplify(Theta=None) → Formula

Compare the parent method Formula.simplify().

>>> from logic1 import Ex, All
>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import x, y, z
>>>
>>> f = And(Eq(x, y), T, Eq(x, y), And(Eq(x, z), Eq(y, x)))
>>> ~ All(x, Ex(y, f)).simplify()
Not(All(x, Ex(y, And(Eq(x, y), Eq(x, z), Eq(y, x)))))

to_nnf(to_positive: bool = True, _implicit_not: bool = False) → Formula

Implements the abstract method Formula.to_nnf().

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

class logic1.firstorder.TruthValue(*args)

Bases: BooleanFormula

A class whose instances are formulas corresponding to \(\top\) and \(\bot\).

print_precedence = 99

A class variable holding the precedence of the operators of instances of TruthValue in LaTeX and string conversions.

This is compared with the corresponding print_precedence of other classes for placing parentheses.

print_style: str = 'constant'

A class variable indicating the use of operators of instances of TruthValue as constants in LaTeX and string conversions.

get_qvars() → set

Implements the abstract method Formula.get_qvars().

get_vars(assume_quantified: set = {}) → GetVars

Implements the abstract method Formula.get_vars().

to_cnf() → Self

Convert to Conjunctive Normal Form.

>>> F.to_dnf()
F

to_dnf() → Self

Convert to Disjunctive Normal Form.

>>> T.to_dnf()
T

to_nnf(to_positive: bool = True, _implicit_not: bool = False) → Formula

Implements the abstract method Formula.to_nnf().

to_sympy()

Raises NotImplementedError since SymPy does not know quantifiers.

final class logic1.firstorder._T

Bases: TruthValue

The constant Formula that is always true.

This is a quite basic implementation of a singleton class. It does not support subclassing. We do not use a module because we need _T to be a subclass itself.

>>> _T() is _T()
True

class property func

A class property yielding the class _T itself.

class property dual_func

A class property yielding the class _F, which implements the dual operator \(\bot\) or \(\top\).

latex_symbol: str = '\\top'

A class variable holding a LaTeX symbol for _T.

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

text_symbol: str = 'T'

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

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

logic1.firstorder.T = _T()

The constant Formula that is always true.

This is a quite basic implementation of a singleton class. It does not support subclassing. We do not use a module because we need _T to be a subclass itself.

>>> _T() is _T()
True

final class logic1.firstorder._F

Bases: TruthValue

The constant Formula that is always false.

This is a quite basic implementation of a singleton class. It does not support subclassing. We do not use a module because we need _F to be a subclass itself.

>>> _F() is _F()
True

class property func

A class property yielding the class _F itself.

class property dual_func

A class property yielding the class _T, which implements the dual operator \(\top\) or \(\bot\).

latex_symbol: str = '\\bot'

A class variable holding a LaTeX symbol for _T.

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

text_symbol: str = 'T'

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

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

logic1.firstorder.F = _F()

The constant Formula that is always false.

This is a quite basic implementation of a singleton class. It does not support subclassing. We do not use a module because we need _F to be a subclass itself.

>>> _F() is _F()
True

class logic1.firstorder.AtomicFormula(*args)

Bases: Formula

class property func

A class property yielding this class or the derived subclass itself.

latex_symbol_spacing = ' '

A class variable holding LaTeX spacing that goes around infix operators.

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

text_symbol_spacing = ' '

A class variable holding spacing that goes around infix operators in string representation.

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

print_precedence = 99

A class variable holding the precedence of latex_symbol and text_symbol with LaTeX and string conversions in subclasses.

This is compared with the corresponding print_precedence of other classes for placing parentheses.

abstract static term_type() → Any

The Python type of terms of the respective subclass of AtomicFormula.

abstract static term_get_vars(term: Any) → set

Extract the set of variables occurring in term.

abstract static term_to_latex(term: Any) → str

Convert term to LaTeX.

abstract static term_to_sympy(term: Any) → sympy.Basic

Convert term to SymPy.

abstract static variable_type() → Any

The Python type of variables in terms in subclasses of AtomicFormula.

abstract static rename_var(variable: Any) → Any

Return a fresh variable for replacing variable in the course of renaming.

Compare Formula.to_distinct_vars(), Formula.to_pnf().

final get_any_atom() → Self

Implements the abstract method Formula.get_any_atom().

final get_qvars() → set

Implements the abstract method Formula.get_qvars().

final to_cnf() → Self

Convert to Conjunctive Normal Form.

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import a
>>>
>>> Eq(a, 0).to_cnf()
Eq(a, 0)

final to_complement() → AtomicFormula

Returns an AtomicFormula equivalent to ~ self.

final to_dnf() → Self

Convert to Disjunctive Normal Form.

>>> from logic1.atomlib.sympy import Eq
>>> from sympy.abc import a
>>>
>>> Eq(a, 0).to_dnf()
Eq(a, 0)

to_nnf(to_positive: bool = True, _implicit_not: bool = False) → Formula

Implements the abstract method Formula.to_nnf().

final to_sympy(**kwargs) → sympy.core.basic.Basic

Override Formula.to_sympy() to prevent recursion into terms.

final transform_atoms(transformation: Callable) → Self

Implements the abstract method Formula.transform_atoms().