george: User Manual

[ Introduction ] [ File Structure ] [ #check PROP ] [ #check PRED ] [ #check PREDTYPES ] [ #check TP ]
[ #check ND ] [ #check ST ] [ Arithmetic ] [ Sets ] [ #check Z ] [ #check PC ]
[ Contributions by Students ] [ Credits ] Keywords ]

Keywords

Identifiers used in george must be of the form letter[letter|number|_]* [!?']?. In other words the identifier must be a letter followed by any number of letters and numbers and underscores. (The !?' characters have special meaning for Z identifiers.) Keywords below may not be used as identifiers.

The following is a list of george's keywords, which cannot be used in identifiers in propositional or predicate logic formulas or labels for proof lines:

(PC) return, do, while, else, then, if, assert, fun, proc
(Z) schema, begin, pred, end, Delta, Xi
(types) nat, pow, int, bool, real
(ND/ST) closed, by, on, for, every, some, assume
(infix operators) in, sube, sub, union, inter, diff, prod
(logical operators) exists, forall

The above are detected by the parser and can only be used in specific places in the grammar. "begin"/"end" are allowed as labels in proofs.

There are a number of other identifiers that george associated with specific types/functions:

(types) nat, real, int, bool
(constants) true, false, empty, univ
(prefix functions) dom, ran, card, id, iter, pow, gen_U, gen_I, iter, compl
(Z schema names) Constants

And george recognizes only certain rules names for TP, ND, ST, and PC.