First-order Framework#
Implementation of first-order formulas over arbitrary signatures and theories.
Throughout this documentation we use the term theory to refer to a choice of function and relation symbols along with their arities (signature) plus a choice of a semantics of those symbols.
An abstract base class Formula
implements representations of and
methods on first-order formulas recursively built using first-order operators:
Boolean operators:
Truth values \(\top\) and \(\bot\)
Negation \(\lnot\)
Conjunction \(\land\) and discjunction \(\lor\)
Implication \(\longrightarrow\)
Bi-implication (syntactic equivalence) \(\longleftrightarrow\)
Quantifiers \(\exists x\) and \(\forall x\), where \(x\) is a variable.
As an abstract base class, Formula
cannot be instantiated.
Nevertheless, it implements a number of properties and methods on first-order
formulas. Those properties and methods are typically syntactic in the sense
that they do not need to know the semantics of the underlying theories.
Boolean operators are implemented as classes derived from another abstract
class BooleanFormula
which is, in turn, derived from
Formula
. Operators are mapped to classes as follows:
\(\top\) |
\(\bot\) |
\(\lnot\) |
\(\land\) |
\(\lor\) |
\(\longrightarrow\) |
\(\longleftrightarrow\) |
The truth values \(\top\) and \(\bot\) are operators of arity 0. As
such, they are implemented as singleton classes _T
and _F
with unique instances T
and F
, respectively.
>>> T is _T()
True
For details on the arities of the other Boolean operators see the documentation of the corresponding classes. On these grounds we can construct formulas based on truth values as follows:
>>> And(Implies(F, T), Or(T, Not(T)))
And(Implies(F, T), Or(T, Not(T)))
More interesting formulas require atomic formulas as another basis of the
recursive construction. This is implemented via another abstract subclass
AtomicFormula
of Formula
,
which provides an interface to various theories via further subclassing.
For some of its methods, AtomicFormula
already provides implementations, which
delegate theory-specific parts to an abstract class
Term
for argument terms of atomic formulas.
We give an example using the theory RCF of Real Closed Fields, which is
implemented not in logic1.firstorder
but in
logic1.theories.RCF
. RCF is the first-order theory of the real numbers
using the signature of ordered rings:
>>> from logic1.theories import RCF
>>> # Assign RCF variables to Python identifiers:
>>> a, b, x = RCF.VV.get('a', 'b', 'x')
>>> # Build formula with first-order operators + RCF variables, functions, relations:
>>> And(x >= 0, a*x + b == 0)
And(x >= 0, a*x + b == 0)
Having learned about variables, we can finally discuss first-order quantifiers
and corresponding quantified formulas. Quantifiers are implemented as classes
derived from another abstract class QuantifiedFormula
which is, in
turn, derived from Formula
. Quantifiers are mapped to classes as
follows:
For details on the arguments of quantifiers see the documentation of the corresponding classes. Here is an example:
>>> from logic1.theories import RCF
>>> a, b, x = RCF.VV.get('a', 'b', 'x')
>>> f = Ex(x, And(x >= 0, a*x + b == 0))
>>> f
Ex(x, And(x >= 0, a*x + b == 0))
Implementations of theories contribute semantic-aware methods and functions on first-order formulas. For instance, quantifier elimination (QE) computes equivalent formulas that do not contain quantifiers anymore:
>>> RCF.qe(f)
Or(And(b == 0, a == 0), And(a != 0, a*b <= 0))
The following class diagram summarizes the inheritance hierarchy.