

Peter Baumgartner and Ulrich Furbach.
Model Elimination without Contrapositives and its
Application to PTTP.
Journal of Automated Reasoning, 13:339359, 1994.
[ bib 
.pdf ]
We give modifications of model elimination which do not
necessitate the use of contrapositives. These restart model
elimination calculi are proven sound and complete and their
implementation by PTTP is depicted. The corresponding proof
procedures are evaluated by a number of runtime experiments
and they are compared to other well known provers. Finally
we relate our results to other calculi, namely the
connection method, modified problem reduction format and
NearHorn Prolog.


Peter Baumgartner.
Refinements of Theory Model Elimination and a Variant
without Contrapositives.
In A.G. Cohn, editor, 11th European Conference on Artificial
Intelligence, ECAI 94. Wiley, 1994.
[ bib 
.pdf ]
Theory Reasoning means to buildin certain knowledge about
a problem domain into a deduction system or calculus, such
as model elimination. We present several complete versions
of highly restricted theory model elimination (TME)
calculi. These restrictions allow (1) to keep fewer path
literals in extension steps than in related calculi, and
(2) to discard proof attempts with multiple occurrences of
literals along a path (i.e. regularity holds). On the
other hand, we obtain by small modifications to TME
versions which do not need contrapositives (à la
NearHorn Prolog). We show how regularity can be adapted
for these versions. The independence of the goal
computation rule holds for all variants. Comparative
runtime results for our PTTPimplementations are supplied.


Peter Baumgartner and Ulrich Furbach.
Model Elimination without Contrapositives.
In A. Bundy, editor, Automated Deduction  CADE12, volume 814
of Lecture Notes in Artificial Intelligence, pages 87101. Springer,
1994.
[ bib 
.pdf ]
We present modifications of model elimination which do
not necessitate the use of contrapositives. These restart
model elimination calculi are proven sound and complete.
The corresponding proof procedures are evaluated by a
number of runtime experiments and they are compared to
other well known provers. Finally we relate our results to
other calculi, namely the connection method, modified
problem reduction format and NearHorn Prolog.


Peter Baumgartner and Ulrich Furbach.
PROTEIN: A PROver with a Theory
Extension Interface.
In A. Bundy, editor, Automated Deduction  CADE12, volume 814
of Lecture Notes in Artificial Intelligence, pages 769773. Springer,
1994.
[ bib 
.pdf ]
PROTEIN (PROver with a Theory
Extension INterface) is a PTTPbased first order
theorem prover over builtin theories. Besides various
standardrefinements known for model elimination, PROTEIN
also offers a variant of model elimination for casebased
reasoning and which does not need contrapositives.


Peter Baumgartner, Jürgen Dix, Ulrich Furbach, and Frieder Stolzenburg.
The Spectrum of Model Elimination based Theorem
Proving.
In C. Walther W. Bibel, editor, Informal Proceedings of the 11th
Annual Meeting of the GIFachgruppe Deduktionssysteme, number AIDA9406 in
Research Report. TH Darmstadt, 1994.
[ bib ]


Peter Baumgartner.
A Transformation Technique to Combine the Linear and the
UnitResulting Restrictions.
In Proceedings of the Eight International Symposium on
Methodologies for Intelligent Systems, Charlotte, N.C, USA, 1994. Oak Ridge
National Laboratory.
[ bib ]


Peter Baumgartner and Ulrich Furbach.
Model Elimination without Contrapositives and its
Application to PTTP.
In Broda D'Agostino Goré Johnson Reeves, editor,
TABLEAUX'94 Workshop, number TR94/5 in Technical Report. Imperial College,
1994.
[ bib ]


Peter Baumgartner and Ulrich Furbach.
Lineare Vervollständigung für die Behandlung von
Horntheorien.
In DFGColloquium “Deduction”, number AIDA9402 in Research
Report. Technische Hochschule Darmstadt, 1994.
[ bib ]


Peter Baumgartner and Ulrich Furbach.
The Spectrum of Model Elimination Based Theorem
Proving.
Proc. of the Workshop “Automated Reasoning: Bridging the Gap between
Theory and Practice”, 1994.
Leeds, England.
[ bib ]


Peter Baumgartner, Ulrich Furbach, and Frieder Stolzenburg.
Applications of Theory Reasoning in Model
Elimination.
In Peter Baumgartner, H.J. Bürckert, H. Comon, Ulrich Furbach,
and Mark Stickel, editors, Theory Reasoning in Automated Deduction,
CADE12 Workshop Proceedings, 1994.
[ bib ]


H.J. Bürckert Peter Baumgartner and H. Comon, editors.
Theory Reasoning in Automated Deduction, 12th International
Conference on Automated Deduction, Workshop. INRIA, Lorraine, 1994.
Technical Report.
[ bib ]


Frieder Stolzenburg and Peter Baumgartner.
Constraint Model Elimination and a
PTTPImplementation.
In R. Yap J. Jourdan, P. Lim, editor, Workshop on Constraint
Languages and their Use in Problem Modelling  International Logic
Programming Symposium, 1994.
[ bib ]