In constraint logic programming, proof procedures for Horn clauses are enhanced with an interface to efficient constraint solvers. In this paper we show how to incorporate constraint processing into a general, non-Horn theorem proving calculus.
A framework for a new calculus is introduced which combines model elimination with constraint solving, following the lines of Bürckert (1991). A prototype system has been implemented rapidly by only combining a PROLOG technology implementation of model elimination and PROLOG with constraints. Some example studies, e.g. taxonomic reasoning, show the advantages and some problems with this procedure.
This paper presents an implementation for the efficient execution of Theory Model Elimination (TME), TME by Linearizing Completion, and Restart Model Elimination (RME) on top of the automated theorem prover SETHEO. These calculi allow for theory reasoning using a Model Elimination based theorem prover. They are described in detail and their major properties are shown. Then, a detailed description how TME by Linearizing Completion and RME can be implemented on top of SETHEO's Abstract Machine (SAM) is given. Due to the flexibility of the Abstract Machine and its input language LOP, only simple transformations of the input formula are sufficient to obtain an efficient implementation. Only for RME, one machine-instruction of the SAM had to be modified slightly. We present results of experiments comparing plain SETHEO with an implementation of TME with PTTP (PROTEIN) and the SETHEO implementation presented here.