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


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.

  • Truth
  • Predicate Application
  • Definedness
  • Equations

  • CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
    Comments to

    Prev Up Next