The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Inductive theorem provers often diverge. This paper describes a critic which monitors the construction of inductive proofs attempting to identify diverging proof attempts. The critic proposes lemmas and generalizations which hopefully allow the proof to go through without divergence. The critic enables the system SPIKE to prove many theorems completely automatically from the definitions alone.
In the field of program synthesis inductive existence proofs are used to compute algorithmic definitions for the skolem functions under consideration. While in general the recursion orderings of the given function definitions form the induction ordering this approach often fail for existence proofs. In many cases a completely new induction ordering has to be invented to prove an existence formula...
A novel approach for automating explicit induction is suggested. Analysis of successful induction proofs reveals that these proofs can be guided without reference to a specific induction axiom. This means that required induction hypotheses can be computed during the proof. We show that some instances of the generalized induction scheme provide induction hypotheses which cannot be obtained using common...
We analyze the search efficiency of a number of common refutational theorem proving strategies for first-order logic. We show that most of them produce search spaces of exponential size even on simple sets of clauses, or else are not sensitive to the goal. We also discuss clause linking, a new procedure that uses a reduction to propositional calculus, and show that it, together with methods that cache...
A previous work on Herbrand model construction is extended in two ways. The first extension increases the capabilities of the method, by extending one of its key rules. The second, more important one, defines a new method for simultaneous search of refutations and models for set of equational clauses. The essential properties of the new method are given. The main theoretical result of the paper is...
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...
We present a procedure for proving inductive theorems which is based on explicit induction, yet supports mutual induction. Mutual induction allows the postulation of lemmas whose proofs use the theorems ex hypothesi while the theorems themselves use the lemmas. This feature has always been supported by induction procedures based on Knuth-Bendix completion, but these procedures are limited by the use...
We show how to prove formulas of the form ∀ x∃ yΦ(x, y) in the initial model of an equational variety by using purely algebraic simplifications. This allows to tackle theorems whose proofs requires complicated noetherian induction. We also give a disproof theorem, which is not only useful to prove that a conjecture is false but is also used to shorten the proof search of a theorem. We show applications...
We study the connection between narrowing and a method for proof by consistency due to Bachmair, and we show that narrowing and proof by consistency may be used to simulate each other. This allows for the migration of results between the two process descriptions. We obtain decidability results for validity of equations in the initial algebra from existing results on narrowing. Furthermore we show...
This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as ‘strictly positive,’ the approach lets definitions involve any operators that have been proved monotone. It is conceptually simple, which has allowed the easy implementation of mutual recursion and other conveniences. It also handles coinductive definitions: simply replace the least fixedpoint...
We define and discuss various conceivable notions of inductive validity for first-order equational clauses. This is done within the framework of constructor-based positive/negative conditional equational specifications which permits to treat negation and incomplete function definitions in an adequate and natural fashion. Moreover, we show that under some reasonable assumptions all these notions are...
Generalisation is currently a major theorem-proving problem. This paper proposes a new method of generalisation, involving the use of explanation-based generalisation within a new domain, which may succeed when other methods fail. The method has been implemented for simple arithmetical examples.
We present a new procedure, semantic hyper-linking, which uses semantics to guide an instance-based clause-form theorem prover. Semantics for the input clauses is given as input. During the search for the proof, ground instances of the input clauses are generated and new semantic structures are built based on the input semantics and a model of the ground clause set. A proof is found if the ground...
Analysis and transformation techniques developed for logic programming can be successfully applied to automatic theorem proving. In this paper we demonstrate how these techniques can prune the search space of the theorem prover, by detecting inference rules and clauses that cannot contribute to proofs. The specialisation techniques developed in this paper are applied to first order clausal theorem...
In this paper we present a method to detect non-provable goals. The general idea, adopted from cycle unification, is to determine in advance how terms may be modified during a derivation. Since a complete predetermination is obviously not possible, we analyze how terms may be changed by, roughly speaking, adding and deleting function symbols. Such changes of a term are encoded by an efficiently decidable...
This paper provides a description of the TPTP library of problems for automated theorem provers. The library is available via Internet, and is intended to form a common basis for the development of and experimentation with automated theorem provers. To support this goal, this paper provides: - the motivations for building the library; - a description of the library structure including...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.