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.
In this paper, we compare different normal form translations from a practical point of view. The usual translation of a closed first-order formula to a disjunctive normal form has severe drawbacks, namely the disruption of the formula's structure and an exponential worst case complexity. In contrast, definitional translations avoid these drawbacks by introducing some additional new predicates yielding...
We present a uniform algorithm fot transforming matrix proofs in classical, constructive, and modal logics into sequent style proofs. Making use of a similarity between matrix methods and Fitting's prefixed tableaus we first develop a procedure for extracting a prefixed sequent proof from a given matrix proof. By considering the additional restrictions on the order of rule applications we then extend...
We present a collection of simple but powerful techniques for enhancing the efficiency of model-generation theorem provers such as Satchmo. The central ideas are to compile a clausal first order theory into a procedural Prolog program and to avoid redundant work of a naïve implementation. We also give an efficient implementation for complement splitting, a method for minimizing the first generated...
This paper develops links between algebra and automated deduction. We show how we have developed heuristics in automated deduction and computer algebra systems by looking at Tietze transformations from group theory and Knuth-Bendix completion. A complex induction proof of a theorem about a wreath product of two groups is developed with the aid of the Larch Prover in order to show how algebraic problems...
Decision procedures are increasingly being employed for deciding or simplifying propositional combinations of ground equalities involving uninterpreted function symbols, linear arithmetic, arrays, and other theories. Two approaches for constructing decision procedures for combinations of ground theories were pioneered in the late seventies. In the approach of Nelson and Oppen, decision procedures...
The shift to semantic symmetries is motivated by the fact that, in contrast with syntactic symmetries, these are preserved under standard inference rules such as resolution. It is then possible to attach groups of semantic symmetries to sets of ground clauses. These groups can provide information useful to inference, as illustrated by three “symmetric” rules. These rules are to be applied in well-defined,...
Forward chaining is an algorithm that is particularly simple, and therefore used in many inference systems. It computes the facts that are the consequences of a set of facts and rules. Unfortunately, this algorithm is not complete with respect to negation. To solve this problem, it is possible, in the context of propositional calculus, to automatically add the rules needed to make forward chaining...
Production rules are a fundamental computational paradigm in artificial intelligence, perhaps being best known as the basis for expert systems. However, to this point there has been little formal study of their properties as a method of deduction. In this paper we initiate such a study by presenting a rewrite semantics for production rule systems. Such a formalization is both interesting per se as...
Problems in automated deduction essentially amount to hard search problems. Powerful search-guiding heuristics are indispensable if difficult problems are to be handled. A promising and natural way to improve the performance of heuristics is to learn from previous experience. We present heuristics that follow this approach. A first heuristic attempts to re-enact a proof of a proof problem found in...
Speculating intermediate lemmas is one of the main reason of user interaction/guidance while mechanically attempting proofs by induction. An approach for generating intermediate lemmas is developed, and its effectiveness is demonstrated while proving properties of recursively defined functions. The approach is guided by the paradigm of attempting to generate a proof of the conclusion subgoal in an...
Indexing techniques support the retrieval and maintenance of large sets of terms. There is also an indexing method called substitution tree indexing that efficiently handles sets of substitutions. We present three advanced indexing operations for substitution trees: The multi-merge for the simultaneous unification of sets of substitutions, the subsumption operation on two sets of substitutions, and...
The method of proving refutational completeness via semantic trees is extended to cope with some new proof search refinements of resolution. It is also shown that a broad class of refinements can be combined with various deletion rules and a strong restriction on factoring without loosing completeness.
The goal of this paper is to propose a new technique for developing decision procedures for propositional modal logics. The basic idea is that propositional modal decision procedures should be developed on top of propositional decision procedures. As a case study, we describe an algorithm, based on an implementation of the Davis-Putnam-Longemann-Loveland procedure, which tests satisfiability in modal...
In this paper a technique is presented which provides us with a means to develop resolution-based calculi for (first-order) modal and temporal logics. The approach is based on three parts: A special translation technique from modal and temporal logic formulae into classical predicate logic, a certain kind of saturation technique which is to be applied to given background theories, and an extraction...
This paper presents a prefixed tableaux calculus for Propositional Dynamic Logic with Converse based on a combination of different techniques such as prefixed tableaux for modal logics and model checkers for mu-calculus. We prove the correctness and completeness of the calculus and illustrate its features. We also discuss the transformation of the tableaux method (naively NEXPTIME) into an EXPTIME...
Tactics are encoded as verifiable meta-functions in a powerful programming logic with reflective capabilities. These formalized tactics are applied to specific problems by means of deductive reflection rules. The main advantage of this approach lies in the fact that meta-theoretic results, once proven, are used without further justification to construct proofs of object-level problems. As another...
Primitive recursion is a well known syntactic restriction on recursive definitions which guarantees termination. Unfortunately many natural definitions, such as the most common definition of Euclid's GCD algorithm, are not primitive recursive. Walther has recently given a proof system for verifying termination of a broader class of definitions. Although Walther's system is highly automatible, the...
We show how a procedure developed by Bledsoe for automatically finding substitution instances for set variables in higher-order logic can be adapted to provide increased automation in proof search in the Calculus of Constructions (CC). Bledsoe's procedure operates on an extension of first-order logic that allows existential quantification over set variables. The method finds maximal solutions for...
In this paper we give and evaluate the algorithms for a fully automated temporal resolution theorem prover. An approach to applying resolution, a proof method for classical logics suited to mechanisation, to temporal logics has been developed by Fisher. As the application of the temporal resolution rule is the most costly part of the method, involving search amongst graphs, we propose different algorithms...
We investigate the problem of finding optimal axiomatizations for operators and distribution quantifiers in finitely-valued first-order logics. We show that the problem can be viewed as the minimization of certain two-valued prepositional formulas. We outline a general procedure leading to optimized quantifier rules for the sequent calculus, for natural deduction and for clause formation. In the case...
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.