CASL/Summary-v1.0 -- 2.3.3.2 Predicate Application

Go backward to 2.3.3.1 Truth
Go up to 2.3.3 Atomic Formulae
Go forward to 2.3.3.3 Definedness

2.3.3.2 Predicate Application

      PREDICATION    ::= predication PRED-SYMB TERMS
      PRED-SYMB      ::= PRED-NAME | QUAL-PRED-NAME
      QUAL-PRED-NAME ::= qual-pred-name PRED-NAME PRED-TYPE
      TERMS          ::= terms TERM*

An application of a predicate symbol PS to some argument terms is written:

PS(T₁, ..., T_n)

When PS is a mixfix identifier, consisting of a sequence `t₀__...__t_n' of tokens or spaces t_i separated by place-holders `__', the application may also be written:

t₀T₁t₁...T_nt_n

When the predicate symbol is a constant with no argument terms, its application is simply written `PS'.

A qualified predicate name QUAL-PRED-NAME with type T is written:

(pred p:T)

An unqualified predicate name PRED-NAME is simply written `p'.

The application of the predicate symbol is well-sorted when there is a declaration of the predicate name (with the argument sorts indicated by the indicated type in the case of a qualified predicate name) such that all the argument terms are well-sorted for the respective argument sorts. It then expands to an application of the qualified predicate name to the fully-qualified expansions of the argument terms for those sorts.

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk