Prev Up Next
Go backward to 2.2 Variable Declarations
Go up to 2 Basic Constructs
Go forward to 2.4 Sort Generation

2.3 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.

2.3.1 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.

2.3.2 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.

2.3.3 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 is  well-sorted, of when a term is well-sorted for a particlar sort, and of the  expansions of atomic formulae and terms, 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 the sentence for false never holds. 

PREDICATION      ::=  predication PRED-SYMB TERMS
PRED-SYMB        ::=  pred-symb PRED-NAME PRED-TYPE?
TERMS            ::=  terms TERM*
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 | 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 TERMS
FUN-SYMB         ::=  fun-symb FUN-NAME FUN-TYPE?
An APPLICATION of a function symbol FUN-SYMB is well-sorted for some particular sort 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, and the result sort is the required sort. 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 for some sort 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: CASL/Summary-v0.97 --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk

Prev Up Next