Basic Specifications

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