Predicate Declarations

$next$ $up$ $previous$ $contents$
Next: Ordering Declarations Up: add: Adding Input Previous: Use Declarations Contents

Predicates that occur in axioms may (but need not) be declared. Only one predicates declaration is allowed in a file.

$\begin{displaymath} \mbox{{\tt predicates(list(PredicateSymbols)).}} \end{displaymath}$

In addition, if

is a binary predicate, by writing

$\begin{displaymath} \mbox{{\tt reflexive\_ {}closure($R1$,$R2$)}}. \end{displaymath}$

one declares

to be the reflexive closure of

. An explicit declaration of the reflexive closure is a shorthand for writing explicitly axioms of the form

$\begin{eqnarray*} R1(X,Y) & \mathrel{\mbox{\tt ->}}& R2(X,Y). \\ R2(X,Y) & \mathrel{\mbox{\tt ->}}& R1(X,Y), X=Y. \end{eqnarray*}$

Harald Ganzinger 2002-12-04