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 ]

Predicate Logic Formulas (#check PRED)

Here is an example of the response to a question that requires a formalization in predicate logic:

#q 03

Formalize the sentence:

Everyone who studies will pass SE212.

#check PRED

forall x. studies(x) => passes(x,SE212)

/*
where
studies(x) means x studies
passes(x,y) means x passes y
*/

george's syntax for predicate logic formulas follows the rules presented in SE212 (e.g., infix, brackets, precedence, and associativity, binding, commas) with the following ASCII symbols for the operators (in addition to those for propositional logic):

Syntax in george	Meaning
forall	forall
exists	exists
=	equality
!=	inequality

There must be spaces around the != as in a != b rather than a!=b or else george may interpret the identifier as a! (which is used for outputs in Z).

george's keywords may not be used as identifiers.

A space is required between the quantifier and the variable name.

What does george check?

For predicate logic formulas, george checks the first non-comment line that follows the directive to make sure:

• The formula is syntactically correct.
• There is an assignment of types to the symbols of the formula that makes it a well-formed formula. Essentially this means that each function, predicate, and constant are all used with consistent arity throughout the formula.

The comments are necessary to inform the TAs of the meanings that you associate with each proposition letter. It does not check multiple formulas - each formula must have a separate #check PRED directive.