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.
Techniques for equational reasoning are a key component in many automated theorem provers and interactive proof and verification systems. A notable recent success in equational theorem proving has been the solution of an open problem (the “Robbins conjecture”) by William McCune with his prover Eqp [13]. Eqp is one of many equational theorem provers that use completion as the main deductive...
In this paper we study the use of commutation properties for proving termination of rewrite systems. Commutation properties may be used to prove termination of a combined system R∪S by proving termination of R and S separately. We present termination methods for ordinary and for equational rewrite systems. Commutation is also important for transformation techniques. We outline the application of transforms—mappings...
We present a completion-like procedure for constructing D-bases for polynomial ideals over commutative Noetherian rings with. unit. The procedure is described at an abstract level, by transition rules. Its termination is proved under certain assumptions about the strategy that controls the application of the transition rules. Correctness is established by proof simplification techniques.
We use the uniform framework of abstract congruence closure to study the congruence closure algorithms described by Nelson and Oppen [9], Downey, Sethi and Tarjan [7], and Shostak [11]. The descriptions thus obtained abstract from certain implementation details while still allowing for comparison between these different algorithms. Experimental results are presented to illustrate the relative efficiency...
We present a graph-based method for constructing a congruence closure of a given set of ground equalities that combines the key ideas of two well-known approaches, completion and abstract congruence closure, in a natural way by relying on a specialized and optimized version of the more general, but less efficient, SOUR graphs. This approach allows for efficient implementations and a visual presentation...
We consider a restricted version of ordered paramodulation, called strict superposition. We show that strict superposition (together with equality resolution) is refutationally complete for Horn clauses, but not for general first-order clauses. Two moderate enrichments of the strict superposition calculus are, however, sufficient to establish refutation completeness. This strictly improves previous...
In this paper we introduce a new class of orderings — associative path orderings — for proving termination of associative commutative term rewriting systems. These orderings are based on the concept of simplification orderings and extend the well-known recursive path orderings to E-congruence classes, where E is an equational theory consisting of associativity and commutativity axioms. The associative...
We show that superposition, a restricted form of paramodulation, can be combined with specifically designed simplification rules such that it becomes a decision procedure for the monadic class with equality. The completeness of the method follows from a general notion of redundancy for clauses and superposition inferences.
We present an extended completion procedure with builtin theories defined by a collection of associativity and commutativity axioms and additional ground equations, and reformulate Buchberger's algorithm for constructing Gröbner bases for polynomial ideals in this formalism. The presentation of completion is at an abstract level, by transition rules, with a suitable notion of fairness used to characterize...
We refine Brand's method for eliminating equality axioms by (i) imposing ordering constraints on auxiliary variables introduced during the transformation process and (ii) avoiding certain transformations of positive equations with a variable on one side. The refinements are both of theoretical and practical interest. For instance, the second refinement is implemented in Setheo and appears to be critical...
We design new inference systems for total orderings by applying rewrite techniques to chaining calculi. Equality relations may either be specified axiomatically or built into the deductive calculus via paramodulation or superposition. We demonstrate that our inference systems are compatible with a concept of (global) redundancy for clauses and inferences that covers such widely used simplification...
We present a new precedence-based termination ordering for (polymorphic) higher-order terms without λ-abstraction. The ordering has been designed to strictly generalize the lexicographic path ordering (on first-order terms). It is relatively simple, but can be used to prove termination of many higher-order rewrite systems, especially those corresponding to typical functional programs. We establish...
In this paper we solve a long-standing open problem by showing that strict superposition—that is, superposition without equality factoring—is refutationally complete. The difficulty of the problem arises from the fact that the strict calculus, in contrast to the standard calculus with equality factoring, is not compatible with arbitrary removal of tautologies, so that the usual techniques for proving...
The replacement of equals by equals is a common form of equational reasoning, of which rewriting is a refinement. Rewrite systems are sets of directed equations, called rewrite rules, that are used for replacements in the indicated direction only. A given expression is rewritten until a simplest possible form, a noremal form, is obtained. Thus, the theory of rewriting is in essence a theory of normal...
We extend previous results on theorem proving for first-order clauses with equality to hierarchic first-order theories. Semantically such theories are confined to conservative extensions of the base models. It is shown that superposition together with variable abstraction and constraint refutation is refutationally complete for sufficiently complete theories. For the proof we introduce a concept of...
We present completion methods for rewriting modulo a congruence, generalizing previous methods by Peterson and Stickel (1981) and Jouannaud and Kirchner (1986). We formalize our methods as equational inference systems and describe techniques for reasoning about such systems.
Use of discrimination nets for many-to-one pattern matching has been shown to dramatically improve the performance of the Knuth-Bendix completion procedure used in rewriting. Many important applications of rewriting require associative-commutative (AC) function symbols and it is therefore quite natural to expect performance gains by using similar techniques for AC-completion. In this paper we propose...
Clause subsumption is of fundamental importance for reducing the search space in theorem proving systems. Since the subsumption problem is NP-complete, the design of efficient heuristics is of significant interest. The core of all subsumption algorithms is the search for suitable substitutions for the variables in a given clause, which in all previously known algorithms is implicitly embedded in the...
This paper presents a sound and complete set of abstract transformation rules for rigid E-unification. Abstract congruence closure, syntactic unification and paramodulation are the three main components of the proposed method. The method obviates the need for using any complicated term orderings and easily incorporates suitable optimization rules. Characterization of substitutions as congruences allows...
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.