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 ]

Typed Predicate Logic Formulas (#check PREDTYPES)

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

#q 03

Formalize the sentence:

Everyone who studies will pass SE212.

#check PREDTYPES

{Person, Course}
SE212:Course
studies: Person --> bool
passes: Person prod Course --> bool

forall x:Person. 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 as is described in #check PRED with the addition that every quantified variable must have a basic type (i.e., forall x:Person . etc).

Multiple formulas or an argument can be listed after the type environment and all will be checked within the same type environment.

Built-in types can be used, but ``univ'' is not allowed as the name of a basic type or within the types of a symbol because ``univ'' is the identifier we use for the set of all objects in untyped predicate logic.

The comments are necessary to inform the TAs of the meanings that you associate with each proposition letter.

What does george check?

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

• Each formula is syntactically correct.
• Each formula typechecks in the type environment described.

george does NOT check:

• that all symbols used in the formula have been given types in the type environment -- it does type inference to ensure there exists a type for the symbol such that the formula passes typechecking
• that the type environment is the most general type