Peter Baumgartner and Ulrich Furbach.
Model Elimination without Contrapositives and its Application to PTTP.
Journal of Automated Reasoning, 13:339-359, 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 Near-Horn 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 build-in 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 Near-Horn 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 PTTP-implementations are supplied.

 
Peter Baumgartner and Ulrich Furbach.
Model Elimination without Contrapositives.
In A. Bundy, editor, Automated Deduction - CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 87-101. 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 Near-Horn Prolog.

 
Peter Baumgartner and Ulrich Furbach.
PROTEIN: A PROver with a Theory Extension Interface.
In A. Bundy, editor, Automated Deduction - CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 769-773. Springer, 1994. [ bib | .pdf ]
PROTEIN (PROver with a Theory Extension INterface) is a PTTP-based first order theorem prover over built-in theories. Besides various standard-refinements known for model elimination, PROTEIN also offers a variant of model elimination for case-based 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 GI-Fachgruppe Deduktionssysteme, number AIDA-94-06 in Research Report. TH Darmstadt, 1994. [ bib ]
 
Peter Baumgartner.
A Transformation Technique to Combine the Linear and the Unit-Resulting 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 TR-94/5 in Technical Report. Imperial College, 1994. [ bib ]
 
Peter Baumgartner and Ulrich Furbach.
Lineare Vervollständigung für die Behandlung von Horntheorien.
In DFG-Colloquium “Deduction”, number AIDA-94-02 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, CADE-12 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 PTTP-Implementation.
In R. Yap J. Jourdan, P. Lim, editor, Workshop on Constraint Languages and their Use in Problem Modelling - International Logic Programming Symposium, 1994. [ bib ]