Peter Baumgartner.
Combining Model Elimination and Unit-Resulting Resolution.
In Proc. Tableau-Workshop, Marseille, 1993.
MPI-Report I-93-213. [ bib ]
 
Peter Baumgartner(Editor).
Workshop PTTP-basiertes Theorembeweisen.
Fachberichte Informatik 7--93, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 1993. [ bib ]
 
Peter Baumgartner.
Refinements of Theory Model Elimination and a Variant without Contrapositives.
Fachberichte Informatik 8/93, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 1993. [ bib ]
 
Peter Baumgartner and Ulrich Furbach.
Consolution as a Framework for Comparing Calculi.
Journal of Symbolic Computation, 16(5):445--477, 1993. [ bib | .pdf ]
In this paper, stepwise and nearly stepwise simulation results for a number of first-order proof calculi are presented and an overview is given that illustrates the relations between these calculi. For this purpose, we modify the consolution calculus in such a way that it can be instantiated to resolution, tableaux model elimination, a connection method and Loveland's model elimination.