Prev Up
Go backward to Predicate Declarations
Go up to 2.1.3 Predicates Predicate Definitions

      PRED-HEAD ::= pred-head ARG-DECL*

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

p (V11, ..., V1m1:s1; ...; Vn1, ..., Vnmn:sn)  <=>  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 s1 (m1 times), ..., sn (mn times). It also asserts the equivalence:

p(V11, ..., Vnmn) <=> 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

Prev Up