**Go backward to** 2.1.3.1 Predicate Declarations

**Go up to** 2.1.3 Predicates

#### 2.1.3.2 Predicate Definitions

PRED-DEFN ::= pred-defn PRED-NAME PRED-HEAD FORMULA
PRED-HEAD ::= pred-head ARG-DECL*

A definition `PRED-DEFN` of a predicate with some arguments is
written:

*p* (*V*_{11}, ...,
*V*_{1m1}:*s*_{1}; ...;
*V*_{n1}, ...,
*V*_{nmn}:*s*_{n}) <=> *F*

When the list of arguments
is empty, the definition is simply written:
*p* <=> *F*

The sign displayed as a double-headed double arrow in LaTeX
is input as ``<=>`'.
It declares the predicate name *p* as a predicate, with a profile
having argument sorts *s*_{1} (*m*_{1} times), ...,
*s*_{n} (*m*_{n} times). It also asserts the equivalence:

*p*(*V*_{11}, ..., *V*_{nmn})
<=> *F*

universally quantified over the declared argument variables
**[CHANGED:]** (which must be distinct, and are the only ones allowed in *T*),
or just `*p* <=> *F*' when the
list of arguments is empty.
**[]** The predicate name *p* may occur in
the formula *F*, and may have *any* interpretation satisfying
the equivalence.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk