BASIC-SPEC ::= basic-spec BASIC-ITEM*
BASIC-ITEM ::= SIG-DECL | VAR-DECL | AXIOM | SORT-GEN
SIG-DECL ::= SORT-DECL | FUN-DECL | PRED-DECL
SORT-DECL ::= sort-decl SORT+
FUN-DECL ::= fun-decl FUN-NAME+ FUN-TYPE
PRED-DECL ::= pred-decl PRED-NAME+ PRED-TYPE
FUN-TYPE ::= fun-type TOTALITY SORT* SORT
TOTALITY ::= total | partial
PRED-TYPE ::= pred-type SORT*
VAR-DECL ::= var-decl VAR+ SORT
AXIOM ::= FORMULA
FORMULA ::= QUANTIFICATION | CONJUNCTION | DISJUNCTION
| IMPLICATION | EQUIVALENCE | NEGATION | ATOM
QUANTIFICATION ::= quantification QUANTIFIER VAR-DECL+ FORMULA
QUANTIFIER ::= forall | exists | exists-uniquely
CONJUNCTION ::= conjunction FORMULA+
DISJUNCTION ::= disjunction FORMULA+
IMPLICATION ::= implication FORMULA FORMULA
EQUIVALENCE ::= equivalence FORMULA FORMULA
NEGATION ::= negation FORMULA
ATOM ::= TRUTH | PREDICATION | DEFINEDNESS | EQUATION
TRUTH ::= true | false
PREDICATION ::= predication PRED-SYMB TERM*
DEFINEDNESS ::= definedness TERM
EQUATION ::= equation QUALITY TERM TERM
QUALITY ::= existential | strong
TERM ::= VAR | APPLICATION | SORTED-TERM
APPLICATION ::= application FUN-SYMB TERM*
SORTED-TERM ::= sorted-term TERM SORT
SORT-GEN ::= sort-gen SORT+ FUN-SYMB+
FUN-SYMB ::= fun-symb FUN-NAME FUN-TYPE?
PRED-SYMB ::= pred-symb PRED-NAME PRED-TYPE?
SORT ::= ID
FUN-NAME ::= ID
PRED-NAME ::= ID
VAR ::= SIMPLE-ID
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk