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

Gleb Frank

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.