Context-free Syntax for Clauses.

Nonterminals in the subsequent grammar are the symbols that begin with an upper-case letter.

Clause  : ProperClause
        | goal ProperClause
        
ProperClause : Antecedent -> Succedent.  -- sequent notation
             | Succedent <- Antecedent.  -- reverse sequents
             | Succedent.                -- positive disjunction
             | axiom( [ AntecedentL, SuccedentL, Constraint ] ).
                                         -- clauses with initial constraints
             | Literals.                 -- Otter-like notation
                
Antecedent : Multiset
Succedent  : []                          -- empty succedent
           | Multiset
Multiset   : Formula ``,'' Multiset | Formula

AntecedentL, SuccedentL: List(Formula)

Literals : Literal OrSymbol Literals
         | Literal

Literal  : Formula                       -- positive literal
         | - Formula                     -- negative literal

OrSymbol : ``;'' | ``|''
        

Formula  : Form
         | Form == Form                  -- equivalence
Form     : all(Variable,Form) 
         | exists(Variable,Form)
         | Form Op Form   
         | ~ Form   
         | Atom
Op       : and | or | => | <=> 

Atom     : Eq 
         | NonEqAtom

Eq       : Term=Term                       -- term equation
         | NonEqAtom                 
NonEqAtom: p(Term,...,Term)    where p is a predicate symbol


Constraint: list( Conjuncts )              -- interpreted as a dnf
Conjunct  : [ List(Ineq) , List(Eq) ]
Ineq      : Term > Term | Term >= Term 

Term      : Prolog term
Variable  : Prolog variable
List(X)   : Prolog list with elements of type X

In addition, the usual Prolog operator precedences apply, plus the following precedences

        :- op(920,yfx,[and]).
        :- op(930,yfx,[or]).
        :- op(950,xfx,[<=>]).
        :- op(950,xfy,[=>]).
        :- op(900,fy,[~,dia,box]).
        :- op(910,yfx,[::]).
        :- op(910,xfx,[^^]).

(The symbols dia, box, ::, and |/TT> are used for denoting modal logic operators in connection with translate.)

Clauses may have ordering and equality constraints attached. (In constraints only term equations are admitted.) In that case a clause represents all the ground instances which satisfy the constraint. The constraints are interpreted over the selected reduction ordering. The ordering is selected by an optional ordering declaration. The constraints mainly serve to reduce the search space for the saturation process and to delay immediate constraint solving upon inference computation. If initial input clauses have constraints refutational theorem proving might be incomplete.

Distinguishing goal clauses (prefix goal) from theory clauses may help in finding proofs faster. Inferences in which at least one premise is derived from a goal clause are selected with higher priority (without violating fairness, however).

There is one important side condition that we make but don't check: [] and [_ |_ ] should not be used as function or predicate symbols. Also, certain symbols, in particular ``not'' and ``:'', that have a meaning on the level of atoms or goals in Prolog programs should not be used. Very strange thing may happen, otherwise.

Imprint | Data Protection