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:

PN (V₁₁, ..., V_1m₁:S₁; ...; V_n1, ..., V_{nm_n}:S_n) <=> F

When the list of arguments is empty, the definition is simply written:

PN <=> F

The sign displayed as a double-headed double arrow in LaTeX is input as `<=>'.

It declares the predicate name PN as a predicate, with a profile having argument sorts S₁ (m₁ times), ..., S_n (m_n times). It also asserts the equivalence:

PN(V₁₁, ..., V_{nm_n}) <=> F

universally quantified over the declared argument variables, or, when the list of arguments is empty, simply:

PN <=> F

The predicate name PN may occur in the formula F, and may have any interpretation satisfying the equivalence.

CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk