A list AXIOM-ITEMS of axioms is written:

axioms F₁; ... F_n;

Each well-formed axiom determines a sentence of the underlying basic specification (closed by universal quantification over all declared variables).

  FORMULA          ::= QUANTIFICATION | CONJUNCTION | DISJUNCTION 
                     | IMPLICATION | EQUIVALENCE | NEGATION | ATOM

A formula is constructed from atomic formulae of the form ATOM using quantification and the usual logical connectives.

Keywords in formulae and terms are displayed in the same font as identifiers (elsewhere in bold face).

2.3.1 Quantifications

2.3.2 Logical Connectives

2.3.2.1 Conjunction

2.3.2.2 Disjunction

2.3.2.3 Implication

2.3.2.4 Equivalence

2.3.2.5 Negation

2.3.3 Atomic Formulae

2.3.3.1 Truth

2.3.3.2 Predicate Application

2.3.3.3 Definedness

2.3.3.4 Equations

2.3.4 Terms

2.3.4.1 Identifiers

2.3.4.2 Qualified Variables

2.3.4.3 Operation Application

2.3.4.4 Sorted Terms

2.3.4.5 Conditional Terms

---

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