We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the basic strategy for narrowing), which forbid paramodulation inferences at terms introduced by substitutions from previous inference steps. In addition we introduce restrictions based on term selection rules and redex orderings, which are general criteria for delimiting the terms which are available for inferences. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences.

This paper studies completion in the case of equations with constraints consisting of first-order formulae over equations, disequations, and an irreducibility predicate. We present several inference systems which show in a very precise way how to take advantage of redundancy notions in this framework. A notable feature of these systems is the variety of trade-offs they present for removing redundant instances of the equations involved in an inference. The irreducibility predicates simulate redundancy criteria based on reducibility (such as prime superposition and Blocking in Basic Completion) and the disequality predicates simulate the notion of subsumed critical pairs; in addition, since constraints are passed along with equations, we can perform hereditary versions of all these redundancy checks. This combines in one consistent framework stronger versions of all practical critical pair criteria. We also provide a rigorous analysis of the problem with completing sets of equations with initial constraints. Finally, an interesting consequence concerning the recalculation of critical pairs in completion procedures is discussed.

In this paper, it is shown that there is an algorithm that, given by finite set E of ground equations, produces a reduced canonical rewriting system R equivalent to E in polynomial time. This algorithm based on congruence closure performs simplification steps guided by a total simplification ordering on ground terms, and it runs in time O(n 3 ) .

In this paper we give a fast method for generating reduced sets of rewrite rules equivalent to a given set of ground equations. Since reduced sets of ground rewrite rules are in fact canonical, this is an efficient Knuth-Bendix procedure for the ground case. The dominant cost of the algorithm is for congruence closure, so the method runs in O(n log n) time and quadratic space, or in O(n (log n)2) time and linear space, where n is the number of occurrences of symbols in the original set of ground equations E. We also show how our method provides a precise characterization of the (finite) collection of all reduced sets of rewrite rules equivalent to a given ground set of equations E, and prove that our algorithm is complete in the sense that it can enumerate every member of this collection. Finally, we show that a modified version of this procedure can produce a reduced ground rewriting system contained in the lexicographic path ordering generated by a given total precedence ordering on the symbols of E , still in a worst-case time of O(n log n).

In this paper, it is shown that the method of matings due to Andrews and Bibel can be extended to (first-order) languages with equality. A decidable version of E -unification called rigid E-unification is introduced, and it is shown that the method of equational matings remains complete when used in conjunction with rigid E -unification. Checking that a family of mated sets is an equational mating is equivalent to the following restricted kind of E -unification. Problem Given E → ={E i | 1≤i≤n} a family of n finite sets of equations and S={〈u i ,v i 〉 |1≤i≤n} a set of n pairs of terms, is there a substitution θ such that, treating each set θ(E i ) as a set of ground equations (i.e., holding the variables in θ(E i ) “rigid”), θ(u i ), and θ(v i ) are provably equal from θ(E i ) for i=1,...,n? Equivalently, is there a substitution θ such that θ(u i ) and θ(v i ) can be shown congruent from θ(E i ) by the congruence closure method for i=1,...,n? A substitution θ solving the above problem is called a rigid E → -unifier of S , and a pair 〈E → ,S〉 such that S has some rigid E → -unifier is called an equational premating. It is shown that deciding whether a pair 〈 E → ,S〉is an equational premating is an NP-complete problem.

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending Andrew's theorem proving method of matings to first-order languages with equality. This extension was first presented by J. H. Gallier, S. Raatz, and W. Snyder, who conjectured that rigid E-unification is decidable. In this paper, it is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are also discussed.

In this paper, we reexamine the problem of general higher-order unification and develop an approach based on the method of transformations on systems of terms which has its roots in Herbrand's thesis, and which was developed by Martelli and Montanari in the context of first-order unification. This method provides an abstract and mathematically elegant means of analyzing the invariant properties of unification in various settings by providing a clean separation of the logical issues from the specification of procedural information. Our major contribution is three-fold. First, we have extended the Herbrand-Martelli-Montanari method of transformations on systems to higher-order unification and pre-unification; second, we have used this formalism to provide a more direct proof of the completeness of a method for higher-order unification than has previously been available; and, finally, we have shown the completeness of the strategy of eager variable elimination. In addition, this analysis provides another justification of the design of Huet's procedure, and shows how its basic principles work in a more general setting. Finally, it is hoped that this presentation might form a good introduction to higher-order unification for those readers unfamiliar with the field.

This paper is concerned with E-unification in arbitrary equational theories. We extend the method of transformations on systems of terms, developed by Martelli-Montanari for standard unification, to E-unification by giving two sets of transformation, BJ and J, which are proved to be sound and complete in the sense that a complete set of E-unifiers for any equational theory E can be enumerated by either of these sets. The set J is an inprovement of BJ, in that many E-unifiers produced by BJ will be weeded out by J. In addition, we show that a generalization of surreduction (also called narrowing) combined with the computation of critical pairs is complete. A new representation of equational proofs as certain kinds of trees is used to prove the completeness of the set BJ in a rather direct fashion that parallels the completeness of the transformations in the case of (standard) unification. The completeness of J and the generalization of surreduction is proved by a method inspired by the concept of unfailing completion, using an abstract (and simpler) notion of the completion of a set of equations.

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending P. Andrews' (1981) theorem-proving method of mating to first-order languages with equality. It is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are discussed.>