Preliminaries

• What This Module Does - An overview of the calculus module's role and abilities.

• How To Include This Module - What to do to make use of the calculus module in a new command-line tool.

Chapter 1: Setting Up

• Calculus Module - Setting up the use of this module.

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

• Binary Predicate Families - To create sets of relations for different purposes.

• Binary Predicate Term Details - To keep track of requirements on the terms for a binary predicate.

• Binary Predicates - To create and manage binary predicates, which are the underlying data structures beneath Inform's relations.

• The Equality Relation - To define that prince among predicates, the equality relation; and also its less noble sidekick, the "has" relation.

• Compilation Schemas - To manage prototype pieces of code for use in code-generation.

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.