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. 

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 | EQUATION
An atomic formula is well-formed (with respect to the current 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 reserved, pre-declared constant predicate symbols, such that true always holds and 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 explicitly-sorted expansions of the term. 

EQUATION        ::=   equation QUALITY TERM TERM
QUALITY         ::=   existential | strong
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 equation on the explicitly-sorted expansions of the terms for that sort. 

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

APPLICATION     ::=   application FUN-SYMB TERM*
FUN-SYMB        ::=   fun-symb FUN-NAME FUN-TYPE?
An application of a function symbol FUN-SYMB is well-sorted when there is a declaration of FUN-SYMB (with the specified FUN-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 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 explicitly-sorted expansions of the component term that have the specified sort.
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk