Prev Up Next
Go backward to 2.2 Variables
Go up to 2 Basic Constructs
Go forward to 2.4 Identifiers

2.3 Axioms

      AXIOM-ITEMS ::= axiom-items AXIOM+     
      AXIOM       ::= FORMULA

A list AXIOM-ITEMS of axioms is written:

axioms F1; ... Fn;

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-v1.0 -- Version: 1.0 -- 22 October 1998.
    Comments to cofi-language@brics.dk

    Prev Up Next