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


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 commandline tool.



Calculus Module  Setting up the use of this module.



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.



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 codegeneration.



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 wellformed sentence in predicate calculus. In this section we reject such propositions on the grounds that they violate typechecking requirements on relations  in this example, the equality relation.



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 runtime without changing their meaning.

Powered by Inweb.