Type Inference

For some reason, I have a feeling we don’t really cover this in CS241E. We introduce a method to do type inference for typed Predicate Logic in SE212.

Type inference is the process of figuring out types for the functions, constants, and variables that make the formula satisfy the rules of typed predicate logic.

Finding the most general typing of a formula (or set of formulas) = using the maximum number of different types such that the formula satisfy the rules of typed predicate logic.

Below are examples of how we do type inference