[
Introduction
]
[
File Structure
]
[
#check PROP
]
[
#check PRED
]
[
#check TP
]
[
#check ND
]
[
#check ST
]
[
Arithmetic
]
[
Sets
]
[
#check Z
]
[
#check PC
]
[
Contributions by Students
]
[
Credits
]
Keywords
]
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.
For predicate logic formulas, george checks the first non-comment line that follows the directive to make sure:
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.