Go backward to Variable Declarations
Go up to Basic Constructs
Go forward to Sort Generation

Axioms and Terms

  AXIOM            ::=  FORMULA
An axiom is well-formed when it is constructed from well-formed atomic formulae (with respect to the local environment), and, moreover, all the variables that occur in it are declared in enclosing quantifications or in variable declarations of the enclosing basic specification. A well-formed axiom determines a sentence of the underlying basic specification (closed by universal quantification over 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.

Quantifiers

  QUANTIFICATION   ::=  quantification QUANTIFIER VAR-DECL+ FORMULA
  QUANTIFIER       ::=  forall | exists | exists-uniquely
A quantification with more than one variable declaration VAR-DECL abbreviates a nest of quantifications with the same quantifier. A quantification with a declaration declaring more than one variable abbreviates a nest of quantifications with the same quantifier and sort. The scope of a variable declaration in a QUANTIFICATION is the component FORMULA, and an inner declaration for a variable with the same identifier as in an outer declaration overrides the outer declaration.

Logical Connectives

  CONJUNCTION      ::=  conjunction FORMULA+
  DISJUNCTION      ::=  disjunction FORMULA+
  IMPLICATION      ::=  implication FORMULA FORMULA
  EQUIVALENCE      ::=  equivalence FORMULA FORMULA
  NEGATION         ::=  negation FORMULA
These formulae determine the usual logical connectives on sub-formulae. Conjunction and disjunction are generalized to lists of formulae FORMULA+, and are only well-formed when the list contains at least two formulae.

Atomic Formulae and Terms

  ATOM             ::=  TRUTH | PREDICATION | DEFINEDNESS 
!                    |  EXISTL-EQUATION | STRONG-EQUATION
An atomic formula 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 or term is  well-sorted and of its  expansion are indicated below for the various constructs. Due to overloading of predicate and/or function symbols, a well-sorted atomic formula or term may have several expansions, preventing it from being well-formed. Qualifications on function 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            ::=  true | false
The atomic formulae true and false are always well-sorted, and expand to primitive sentences, such that the sentence for true always holds, and that for false never holds. 

  PREDICATION      ::=  predication PRED-SYMB TERM*
  PRED-SYMB        ::=  pred-symb PRED-NAME PRED-TYPE?
An application of a predicate symbol PRED-SYMB is well-sorted when there is a declaration of PRED-SYMB (with the specified PRED-TYPE, if any) such that all the argument terms are well-sorted for the declared argument sorts. It then expands to an application of the qualified predicate symbol to the fully-qualified expansions of the argument terms for those sorts. 

  DEFINEDNESS      ::=  definedness TERM
A definedness formula is well-sorted when the term is well-sorted for some sort. It then expands to a definedness assertion on the fully-qualified expansion of the term. 

! EXISTL-EQUATION  ::=  existl-equation TERM TERM
! STRONG-EQUATION  ::=  strong-equation TERM TERM
An equation is well-sorted if there is a sort such that both the terms are well-sorted for that sort. It then expands to the corresponding existential or strong equation on the fully-qualified expansions of the terms for that sort. 

! TERM             ::=  VAR | CONSTANT | APPLICATION | SORTED-TERM
A variable VAR is well-sorted for the sort specified in its declaration; it expands to the variable itself. 

! CONSTANT         ::=  FUN-SYMB
! APPLICATION      ::=  application FUN-SYMB TERM+
  FUN-SYMB         ::=  fun-symb FUN-NAME FUN-TYPE?
A CONSTANT is well-sorted when the FUN-SYMB is declared as a constant (with a particular FUN-TYPE, if specified); it expands to an application of the fully-qualified function symbol to no arguments.

An APPLICATION of a function symbol FUN-SYMB is well-sorted when there is a declaration of FUN-SYMB (with a particular FUN-TYPE, if specified) such that all the argument terms are well-sorted for the declared argument sorts. It then expands to an application of the qualified function symbol to the fully-qualified expansions of the argument terms for those sorts. 

  SORTED-TERM      ::=  sorted-term TERM SORT
A sorted term is well-sorted if the component term is well-sorted for the specified sort. It then expands to those of the fully-qualified expansions of the component term that have the specified sort.
CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk