Abstracts of selected research reports

Elimination of Equality via Transformation with Ordering Constraints

Bachmair, L. and Ganzinger, H. and Voronkov, A.

Abstract: 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 the right-hand side. The refinements are both of theoretical and practical interest. For instance, the second refinement is implemented in Setheo and appears to be critical for that prover's performance on equational problems. The correctness of this variant of Brand's method was an open problem that is solved by the more general results in the present paper. The experimental results we obtained from a prototype implementation of our proposed method for the model elimination prover Protein also show some dramatic improvements of the proof search. Ordering constraints have already been widely used in equational theorem provers based on paramodulation. We prove the correctness of our refinements of Brand's method by establishing a suitable connection to basic paramodulation calculi and thereby shed new light on the connection between different approaches to equational theorem proving.

Bachmair, L. and Ganzinger, H.

Abstract: The most efficient techniques that have been developed to date for equality handling in first-order theorem proving are based on superposition calculi. Superposition is a refinement of paramodulation in that various ordering constraints are imposed on inferences. For practical purposes, a key aspect of superposition is its compatibility with powerful simplification techniques. 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 (refutational) completeness of paramodulation calculi are not directly applicable. We deal with the problem by introducing a suitable notion of {\em direct rewrite proof\/} and modifying proof techniques based on candidate models and counterexamples in that we define these concepts, not in terms of semantic truth, but in terms of direct provability. We also introduce a corresponding concept of redundancy with which strict superposition is compatible and that covers most simplification techniques, though not, of course, removal of {\em all\/} tautologies. Reasoning about the strict calculus, it turns out, requires techniques known from the more advanced {\em basic\/} variant of superposition. Superposition calculi, in general, are parametrized by (well-founded) literal orderings. We prove refutational completeness of strict basic superposition for a large class of such orderings. For certain orderings, positive top-level superposition inferences {\em from\/} variables turn out to be redundant---a result that is relevant, surprisingly, in the context of equality elimination methods. The results are also extended to chaining calculi for non-symmetric transitive relations.

Bachmair, L. and Ganzinger, H.

Abstract: We review the fundamental resolution-based methods for first-order theorem proving and present them in a uniform framework. We show that these calculi can be viewed as specializations of non-clausal resolution with simplification. Simplification techniques are justified with the help of a rather general notion of redundancy for inferences. As simplification and other techniques for the elimination of redundancy are indispensable for an acceptable behaviour of any practical theorem prover this work is the first uniform treatment of resolution-like techniques in which the avoidance of redundant computations attains the attention it deserves. In many cases our presentation of a resolution method will indicate new ways of how to improve the method over what was known previously. We also give answers to several open problems in the area.

Ganzinger, H. and Waldmann, U.

Abstract: We describe a refined superposition calculus for cancellative abelian monoids. They encompass not only abelian groups, but also such ubiquitous structures as the natural numbers or multisets. Both the AC axioms and the cancellation law are difficult for a general purpose superposition theorem prover, as they create many variants of clauses which contain sums. Our calculus requires neither explicit inferences with the theory clauses for cancellative abelian monoids nor extended equations or clauses. Improved ordering constraints allow us to restrict to inferences that involve the maximal term of the maximal sum in the maximal literal. Furthermore, the search space is reduced drastically by certain variable elimination techniques.

Bachmair, L. and Ganzinger, H.

Abstract: We propose inference systems for binary relations with composition laws of the form $S\circ T\subseteq U$ in the context of resolution-type theorem proving. Particulary interesting examples include transitivity, partial orderings, equality and the combination of equality with other transitive relations. Our inference mechanisms are based on standard techniques from term rewriting and represent a refinement of chaining methods. We establish their refutational completeness and also prove their compatibility with the usual simplification techniques used in rewrite-based theorem provers. A key to the practicality of chaining techniques is the extent to which so-called variable chainings can be restricted. We demonstrate that rewrite techniques considerably restrict variable chaining, though we also show that they cannot be completely avoided in general. If a binary relation under consideration satisfies additional properties, such as symmetry, further restrictions are possible. In particular, we discuss orderings and partial congruence relations.

Basin, D. and Ganzinger, H.

Abstract: We define \emph{order locality} to be a property of clauses relative to a term ordering. This property is a generalization of the subformula property for proofs where terms arising in proofs are bounded, under the given ordering, by terms appearing in the goal clause. We show that when a clause set is order local, then the complexity of its ground entailment problem is a function of its structure (e.g., full versus Horn clauses), and the ordering used. We prove that, in many cases, order locality is equivalent to a clause set being saturated under ordered resolution. This provides a means of using standard resolution theorem provers for testing order locality and transforming non-local clause sets into local ones. We have used the Saturate system to automatically establish complexity bounds for a number of nontrivial entailment problems relative to complexity classes which include Polynomial and Exponential Time and co-NP.

[an error occurred while processing this directive]