**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*_{1}, ..., *T*_{n})

When *PS* is a mixfix identifier, consisting of a sequence
`*t*_{0}__...__*t*_{n}' of tokens or spaces
*t*_{i} separated by place-holders `*__*', the application
may also be written:
*t*_{0}*T*_{1}*t*_{1}...*T*_{n}*t*_{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