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