Prev Up Next
Go backward to 2.3.2 Logical Connectives
Go up to 2.3 Axioms
Go forward to 2.3.4 Terms

2.3.3 Atomic Formulae

  ATOM             ::= TRUTH | PREDICATION | DEFINEDNESS 
                     | EXISTL-EQUATION | STRONG-EQUATION

An atomic formula ATOM is well-formed (with respect to the local environment and variable declarations) if it is well-sorted and expands to a unique atomic formula for constructing sentences. The notions of when an atomic formula is  well-sorted, of when a term is well-sorted for a particular sort, and of the  expansions of atomic formulae and terms, are indicated below for the various constructs.

Due to overloading of predicate and/or operation symbols, a well-sorted atomic formula or term may have several expansions, preventing it from being well-formed. Qualifications on operation and predicate symbols may be used to determine the intended expansion and make it well-formed; explicit sorts on arguments and/or results may also help to avoid unintended expansions.

  • 2.3.3.1 Truth
  • 2.3.3.2 Predicate Application
  • 2.3.3.3 Definedness
  • 2.3.3.4 Equations

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

    Prev Up Next