SETHEO and E-SETHEO - The CADE-13 Systems
Journal of Automated ReasoningPublished 1 April 1997
Max Moser, Ortrun Ibens, Reinhold Letz, Joachim P. Steinbach, Christoph Goller, Johann Schumann
Citations82
SJR quartileQ2
SJR score0.62
SNIP1.15
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
An overview of the theoretical background, the system architecture, and the performance of both model elimination theorem prover SETHEO and its equational extension E-SETHEO are presented.
Abstract
The model elimination theorem prover SETHEO (version V3.3) and its equational extension E-SETHEO are presented. SETHEO employs sophisticated mechanisms of subgoal selection, elaborate iterative deepening techniques, and local failure caching methods. Its equational counterpart E-SETHEO transforms formulae containing equality (using a variant of Brand's modification method) and processes the output with the standard SETHEO system. This article gives an overview of the theoretical background, the system architecture, and the performance of both systems.
Keywords
Computer Science
Journal of the ACMA Machine-Oriented Logic Based on the Resolution Principle
3,885 Citations1965John A. Robinson
The paper concludes with a discussion of several principles which are applicable to the design of efficient proof-procedures employing resolution as the basle logical process.
Simple Word Problems in Universal Algebras
1,373 Citations1983Donald E. Knuth, PETER B. BENDIX
First-Order Logic
677 Citations1968Raymond M. Smullyan
Elsevier eBooksSimple Word Problems in Universal Algebras††The work reported in this paper was supported in part by the U.S. Office of Naval Research.
468 Citations1970Donald E. Knuth, PETER B. BENDIX
Automated Theorem Proving
461 Citations1987Wolfgang Bibel
Methods of theorem proving in propositional logic are presented first, and then methods for first-order logic, and a brief introduction to propositional and first-order logic is given.
Paramodulation and Theorem-Proving in First-Order Theories with Equality
271 Citations1983George Robinson, L. Wos
Journal of Automated ReasoningA prolog technology theorem prover: Implementation by an extended prolog compiler
249 Citations1988Mark E. Stickel
A Prolog technology theorem prover is an extension of Prolog that is complete for the full first-order predicate calculus that differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and depth-first iterative-deepening search instead of unbounded depthfirst search to makethe search strategy complete.
Journal of Automated ReasoningSETHEO: A high-performance theorem prover
237 Citations1992Reinhold Letz, J. Schümann +2 more
A sound and complete theorem prover for first-order logic is presented, which is based on the connection method, and incorporates a powerful preprocessing module for a reduction of the input formula.
Lecture notes in computer scienceThe TPTP problem library
166 Citations1994Geoff Sutcliffe, Christian Suttner +1 more
Journal of Automated ReasoningControlled integration of the cut rule into connection tableau calculi
153 Citations1994Reinhold Letz, Klaus Mayr +1 more
Techniques are developed and compared that increase the inferential power of tableau systems for classical first-order logic and develop and apply an extension of the regularity condition on tableaux and the mechanism of anti-lemmata which realizes a subsumption concept on tableau.
SIAM Journal on ComputingProving Theorems with the Modification Method
145 Citations1975Daniël Brand
Completeness of this “Modification Method” implies completeness of Paramodulation without the functionally reflexive axioms, thus proving a conjecture of Wos and Robinson (1969), and holds with some other restrictions, such as limiting paramodulation into variables.
Information and ComputationBasic Paramodulation
128 Citations1995Leo Bachmair, Harald Ganzinger +2 more
It is proved that refutational completeness in the context of deletion rules, such as simplification by rewriting and subsumption, and of techniques for eliminating redundant inferences, is complete without paramodulation into variables or using functional reflexivity axioms.
Journal of Automated ReasoningOtter - The CADE-13 Competition Incarnations
104 Citations1997William McCune, Larry Wos
The two incarnations of Otter entered in the CADE-13 Automated Theorem Proving System Competition are discussed, with some historical background and a summary of applications that have led to new results in mathematics and logic.
Theoretical Computer ScienceComplete sets of transformations for general E-unification
103 Citations1989Jean Gallier, Wayne Snyder
This thesis presents the first rigorous analysis of a method for E-unification which is fully general in the sense that it is capable of enumerating a complete set of E- unifiers for arbitrary sets of equations E.
Artificial IntelligenceRefutation graphs
97 Citations1976Robert E. Shostak
A graph-theoretic characterization of truth-functional consistency is introduced, providing a clear perspective on some resolution-based for deciding formulas in propositional and first-order logic.
Lecture notes in computer scienceCaching and lemmaizing in model elimination theorem provers
75 Citations1992Owen Astrachan, Mark E. Stickel
This paper reports on work done to modify a model elimination theorem prover using two techniques, caching and lemmaizing, that have reduced by more than an order of magnitude the time required to find proofs of several problems and that have enabled the prover to prove theorems previously unobtainable by top-down model eliminationorem provers.
Lecture notes in computer scienceOptimizing proof search in model elimination
54 Citations1996John Harrison
An optimized version of this search mode of model elimination is proposed using a simple divide-and-conquer refinement, and optimized and unoptimized modes are compared, together with depth-bounded and best-first search, over the entire TPTP problem library.
The Knowledge Engineering ReviewAutomated theorem proving (second revised edition) by Wolfgang Bibel, Vieweg1987.
39 Citations1988G. A. Ringwood
The book ought at least to wet the appetite of the manager curious to learn a little more of expert systems, and the inclusion of the contextual factors as essential ingredients in successful expert system implementation is encouraging.
Journal of Automated ReasoningThe Results - of the CADE-13 ATP System Competition
19 Citations1997Geoff Sutcliffe, Christian Suttner
The CADE-13 ATP System Competition tested 18 ATP systems on 50 theorems, in five competition categories, with a time limit of 300 seconds imposed on each system run, and some analysis of these results is given.
Lecture notes in computer scienceSubgoal alternation in model elimination
14 Citations1997Ortrun Ibens, Reinhold Letz
This paper shows that the standard selection methods are not flexible enough to satisfy this principle, and as a generalization of the standard paradigm the new method of subgoal alternation is presented and integrated into the theorem prover SETHEO.
Lecture notes in computer scienceImproving transformation systems for general E-unification
7 Citations1993Max Moser
A new and improved transformation system for general E-unification is motivated and presented as a modification of the original transformation system by Gallier and Snyder refined by ordinary unification and basic paramodulation and an important property is shown: independence of the selection rule.