CASL/Summary -- 2.1.3.2 Predicate Definitions

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₁₁, ..., v_1m₁:s₁; ...; v_n1, ..., v_{nm_n}: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₁ (m₁ times), ..., s_n (m_n times). It also asserts the equivalence:

p(v₁₁, ..., v_{nm_n}) <=> F

universally quantified over the declared argument variables (which must be distinct, and are the only ones allowed in F), 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 -- Version: 1.0 -- 22 July 1999.
Comments to cofi-language@brics.dk