CASL/Summary-v1.0 -- 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 [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