A General Interface for Interaction of Special-Purpose Reasoners within a Modular Reasoning System

Contents

The increasing significance of special-purpose reasoners in theorem proving, and the necessity for a common interaction interface for such reasoners is discussed. A candidate set of operations for such an interface is proposed. The interface is based on two important classes of objects - a reasoner and a proof step. A discussion on the importance of presenting proofs in flexible, human-readable format follows. We conclude by a general description of JTP, a model elimination theorem prover constructed using the presented interface.