Formula Syntax

First-order formulas are built in from

• Prolog variables, denoting free or bound variables,
• logical symbols =, ~, and, or, <=>, =>, all, and exists, denoting equality, negation, conjunction, disjunction, equivalence, implication, universal and existential quantification, respectively, and
• Prolog terms for denoting terms and atoms.

General or standard first-order clauses are written as sequents $\Gamma \mathrel{\mbox{\tt ->}}\Delta$ of multisets $\Gamma$ (the antecedent) and $\Delta$ (the succedent) of general literals. The elements in $\Gamma$ and $\Delta$ are separated by ``,''. A general literal is either a first-order formulas $F$ or, somewhat unusually, an equality $F\mathrel{\mbox{{\tt ==}}}G$ between two formulas $F$ and $G$. As usual, comma on the right side of $\mathrel{\mbox{\tt ->}}$ denotes disjunction, and comma left denotes conjunction. Equality on the level of formulas denotes logical equivalence. This is an example of a sequent consisting of a single (and positive) equality:

   -> eq(X,Y) == all(Z,member(Z,X) <=> member(Z,Y))

Free variables in a clause, such as $X$ and $Y$ above, are implicitly universally quantified. Here is an example of a (Horn) sequent

   exists(X,f(X)), exists(X,g(X)) ->
         all(X,(f(X) => h(X)) and all(X,g(X)=>j(X)))
                             == 
         all(X,all(Y,f(X) and g(Y) => h(X) and j(Y)))

with a 2-element antecedent and an $\mathrel{\mbox{{\tt ==}}}$-equality as succedent. We have an equivalence == on the level of sequents (in addition to the equivalence <=> on the level of formulas) as an explicit indication for our computing with certain such equivalences by rewriting. A detailed definition of the syntax is given below.

Imprint | Data Protection