Peter Baumgartner, Reiner Hähnle, and J. Posegga, editors.
Theorem Proving with Analytic Tableaux and Related Methods, volume 918 of Lecture Notes in Artificial Intelligence. Springer, 1995. [ bib ]
 
Peter Baumgartner and Frieder Stolzenburg.
Jahrestreffen der GI-Fachgruppe 1.2.1 Deduktion.
KI, 9(6):80--81, 1995.
Conference report. [ bib ]
 
Peter Baumgartner and Johann Schumann.
Implementing Restart Model Elimination and Theory Model Elimination on top of SETHEO.
Fachberichte Informatik 5--95, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 1995. [ bib | .ps.gz ]
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.
 
Peter Baumgartner, Ulrich Furbach, and Frieder Stolzenburg.
Computing Answers and Logic Programming by Model Elimination Based Theorem Proving.
Proc. of the Workshop “Automated Reasoning: Bridging the Gap between Theory and Practice”, 1995.
Leeds, England. [ bib ]
 
Peter Baumgartner and Frieder Stolzenburg.
Constraint Model Elimination and a PTTP-Implementation.
In Baumgartner et al. [1], pages 201--216. [ bib | .pdf ]
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.