Storing and simplifying propositions in predicate calculus. This is version 1.

• Preliminaries

• Chapter 1: Setting Up

• Chapter 2: Unary Predicates

• Unary Predicates - A lightweight structure to represent a unary predicate, which is either true or false when applied to a single term.

• Unary Predicate Families - To create sets of unary predicates for different purposes.

• Kind Predicates - To define the predicates for membership of a kind.

• Chapter 3: Binary Predicates

• Chapter 4: Propositions

• Terms - Terms are the representations of values in predicate calculus: variables, constants or functions of other terms.

• Atomic Propositions - To build and modify atoms, the syntactic pieces from which propositions are built up.

• Propositions - To build and modify structures representing propositions in predicate calculus.

• Binding and Substitution - To substitute constants into propositions in place of variables, and to apply quantifiers to bind any unbound variables.

• Type Check Propositions - Predicate calculus is a largely symbolic exercise, and its rules of working tend to assume that all predicates are meaningful for all terms: this means, for instance, that "if blue is 14" is likely to make a well-formed sentence in predicate calculus. In this section we reject such propositions on the grounds that they violate type-checking requirements on relations -- in this example, the equality relation.

• Chapter 5: Sentences

• Sentence Conversions - Turning parse trees from English sentences into logical propositions.

• Simplifications - A set of operations which rewrite propositions to make them easier or quicker to test at run-time without changing their meaning.