RelAPS (Relation Algebraic Proof System) is an interactive system assisting in proving relation-algebraic theorems. The goal of the system is to provide an environment where a user can perform a relation-algebraic proof similar to doing it using pencil and paper. The system ensures that an individual proof-step is executed properly, while it remains the responsibility of the user to complete the proof.
RelAPS is based on the theory of allegories. The system was designed to handle extensions of that theory such as distributive allegories, division allegories and so on. The distribution below contains the latter theories. Any further extension can easily be added.
A lot of proofs in the theory of relations are either based on equational and/or inclusion based reasoning or on a chain of equivalences. The RelAPS system has a special `working area' to perform proofs in that style. In such a proof humans usually use certain properties of operations and predicates without mentioning. These properties are commutatvity, associative, and monotinicity of operations and symmetry, and transitivity of binary predicates. The RelAPS system is capable of recognizing these proprties, and to apply them automatically.
In order to mimic human reasoning above the equational calculations, the system is based on a specific version of natural deduction. This version keeps assumptions local while still working with exactly one conclusion in the proof.
The system can be downloaded using the link below. It requires a working version of Java on the target machine. An installation is not necessary. After unzipping the file just call RelAPS.jar.