-
-
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.