Abstracts of selected conference papers

New Directions in Instantiation-Based Theorem Proving

Ganzinger, H. and Korovin, K.

Abstract: We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences and where inconsistency is detected by propositional tests. We give a model construction proof of completeness by which restricted inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation.

Ganzinger, H. and Hillenbrand, T. and Waldmann, U.

Abstract: We investigate superposition modulo a Shostak theory $T$ in order to facilitate reasoning in the amalgamation of $T$ and a free theory~$F$. % Free operators occur naturally for instance in program verification problems when abstracting over subroutines. If their behaviour in addition can be specified axiomatically, much more of the program semantics can be captured. % Combining the Shostak-style components for deciding the clausal validity problem with the ordering and saturation techniques developed for equational reasoning, we derive a refutationally complete calculus on mixed ground clauses which result for example from CNF transforming arbitrary universally quantified formulae. % The calculus works modulo a Shostak theory in the sense that it operates on canonizer normalforms. For the Shostak solvers that we study, coherence comes for free: no coherence pairs need to be considered.

Ganzinger, H. and Stuber, J.

Abstract: The paper describes a superposition calculus where quantifiers are eliminated lazily. Superposition and simplification inferences may employ equivalences that have arbitrary formulas at their smaller side. A closely related calculus is implemented in the Saturate system and has shown useful on many examples, in particular in set theory. The paper presents a completeness proof and reports on practical experience obtained with the Saturate system.

Ganzinger, H. and McAllester, D.

Abstract: It is widely accepted that many algorithms can be concisely and clearly expressed as logical inference rules. However, logic programming has been inappropriate for the study of the running time of algorithms because there has not been a clear and precise model of the run time of a logic program. We present a logic programming model of computation appropriate for the study of the run time of a wide variety of algorithms.

Ganzinger, H.

Abstract: We represent the essential ingredients of Shostak's procedure at a high level of abstraction, and as a refinement of the Nelson-Oppen procedure. We analyze completeness issues of the method based on a general notion of theories. We also formalize a notion of sigma-models and show that on the basis of Shostak's procedure we cannot distinguish a theory from its approximation represented by the class of its sigma-models.

Ganzinger, H.

Abstract: In this paper we compare three approaches to polynomial time decidability for uniform word problems for quasi-varieties. Two of the approaches, by Evans and Burris, respectively, are semantical, referring to certain embeddability and axiomatizability properties. The third approach is proof-theoretic in nature, inspired by McAllester's concept of local inference. We define two closely related notions of locality for equational Horn theories and show that both the criteria by Evans and Burris lie in between these two concepts. In particular, our notion of weak locality subsumes both Evans' and Burris' method.

Ganzinger, H. and McAllester, D.

Abstract: Nontrivial meta-complexity theorems, proved once for a programming language as a whole, facilitate the presentation and analysis of particular algorithms. This paper gives a new meta-complexity theorem for bottom-up logic programs that is both more general and more accurate than previous such theorems. The new theorem applies to algorithms not handled by previous meta-complexity theorems, greatly facilitating their analysis.

Ganzinger, H. and Nieuwenhuis, R. and Nivela, P.

Abstract: Indexing data structures have a crucial impact on the performance of automated theorem provers. Examples are discrimination trees, which are like tries where terms are seen as strings and common prefixes are shared, and substitution trees, where terms keep their tree structure and all common contexts can be shared. Here we describe a new indexing data structure, called context trees, where, by means of a limited kind of context variables, also common subterms can be shared, even if they occur below different function symbols. Apart from introducing the concept, we also provide evidence for its practical value. We describe an implementation of context trees based on Curry terms and on an extension of substitution trees with equality constraints, where one also does not distinguish between internal and external variables. Experiments with matching benchmarks show that our preliminary implementation is already competitive with tightly coded current state-of-the-art implementations of the other main techniques. In particular space consumption of context trees is significantly less than for other index structures.

Ganzinger, Harald and Hustadt, Ullrich and Meyer, Christoph and Schmidt, Renate A.

Abstract: This paper presents a resolution decision procedure for transitive propositional modal logics. The procedure combines the relational translation method with an ordered chaining calculus designed to avoid unnecessary inferences with transitive relations. We show the logics K4, KD4 and S4 can be transformed into a bounded class of well-structured clauses closed under ordered resolution and negative chaining.

Ganzinger, H. and Sofronie-Stokkermans, V.

Abstract: We apply chaining techniques to automated theorem proving in many-valued logics. In particular, we show that superposition specializes to a refined version of the many-valued resolution rules introduced by Baaz and Fermüller, and that ordered chaining can be specialized to a refutationally complete inference system for regular clauses.

Ganzinger, H. and De Nivelle, H.

Abstract: We give a decision procedure for the guarded fragment with equality. The procedure is based on resolution with superposition. The relevance of the guarded fragment lies in the fact that many modal logics can be translated into it. In this way the guarded fragment acts as a framework explaining some of the nice properties of these modal logics. By constructing an implementable decision procedure for the guarded fragments we define an effective procedure for deciding these modal logics. It is surprising to see that one does not need any sophisticated simplification and redundancy elimination method to make superposition terminate on the class of clauses that is obtained from the clausification of guarded formulas. Yet the decision procedure obtained is optimal with regard to time complexity.

Ganzinger, H. and Meyer, Chr. and Veanes, M.

Abstract: We consider the restriction of the guarded fragment to the two-variable case where, in addition, binary relations may be specified as transitive. We show that (i) this very restricted form of the guarded fragment without equality is undecidable and that (ii) when allowing transitive relations other than equality to occur only in guards, the logic becomes decidable. The latter subclass of the guarded fragment is the one that occurs naturally when translating multi-modal logics of the type K4, S4 or S5 into first-order logic. We also show that the loosely guarded fragment with a single transitive relation is undecidable.

Cortier, V. and Ganzinger, H. and Jacquemard, F. and Veanes, M.

Abstract: In this paper we prove decidability results of restricted fragments of simultaneous rigid reachability or SRR, that is the nonsymmetrical form of simultaneous rigid E-unification or SREU. The absence of symmetry enforces us to use different methods, than the ones that have been successful in the context of SREU (for example word equations). The methods that we use instead, involve finite (tree) automata techniques, and the decidability proofs provide precise computational complexity bounds. The main results are 1) monadic SRR with ground rule is PSPACE-complete, and 2) balanced SRR with ground rules is EXPTIME-complete. These upper bounds have been open already for corresponding fragments of SREU, for which only the hardness results have been known. The first result indicates the difference in computational power between fragments of SREU with ground rules and nonground rules, respectively, due to a straightforward encoding of word equations in monadic SREU (with nonground rules). The second result establishes the decidability and precise complexity of the largest known subfragment of nonmonadic SREU.

Bachmair, L. and Ganzinger, H.

Abstract: 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 introduce a corresponding concept of redundancy with which strict superposition is compatible and that covers most simplification techniques.

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.

Ganzinger, H. and Jacquemard, F. and Veanes, M.

Abstract: We show that rigid reachability, the non-symmetric form of rigid $E$-unification, is undecidable already in the case of a single constraint. From this we infer the undecidability of a new rather restricted kind of second-order unification. We also show that certain decidable subclasses of the problem which are \PTIME-complete in the equational case become \EXPTIME-complete when symmetry is absent. By applying automata-theoretic methods, simultaneous monadic rigid reachability with ground rules is shown to be in \EXPTIME.

Ganzinger, H. and Meyer, Chr. and Weidenbach, Chr.

Abstract: We propose a variant of ordered resolution with semantic restrictions based on interpretations which are identified by the given atom ordering and selection function. Techniques for effectively approximating validity (satisfiability) in these interpretations are presented. They are related to methods of soft typing for programming languages. The framework is shown to be strictly more general than certain previously introduced approaches. Implementation of some of our techniques in the SPASS prover has lead to encouraging experimental results.

Basin, D. and Ganzinger, H.

Abstract: McAllester and Given have given procedures for recognizing certain sets of Horn clauses which generate polynomial time decidable entailment relations. These clause sets have a property called {\em locality}, which corresponds to a kind of subformula property for Horn clause proofs. We generalize locality and show that it is in many cases equivalent to a clause set being saturated up to redundancy under ordered resolution. This provides a procedure, which we have implemented in the Saturate system, for testing locality and transforming non-local clause sets into local ones. Our notion of locality is defined on full clauses and is relative to term-orderings; this allows us to use Saturate to automatically establish complexity bounds for entailment problems and algorithms relative to a variety of complexity classes, including PTime, co-NP, and Exponential Time.

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 dealing with transitive relations in the context of resolution-type theorem proving. These 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 for transitive relations in general. If the given relation satisfies additional properties, such as symmetry, further restrictions are possible. In particular, we discuss (partial) equivalence relations and congruence relations.

Bachmair, L. and Ganzinger, H.

Abstract: We present an associative-commutative paramodulation calculus that generalizes the associative-commutative completion procedure to first-order clauses. The calculus is parametrized by a selection function (on negative literals) and a well-founded ordering on terms. It is compatible with an abstract notion of redundancy that covers such simplification techniques as tautology deletion, subsumption, and simplification by (associative-commutative) rewriting. The proof of refutational completeness of the calculus is comparatively simple, and the techniques employed may be of independent interest.

Bachmair, L. and Ganzinger, H. and Stuber, J.

Abstract: We present a general approach for integrating certain mathematical structures in first-order equational theorem provers. More specifically, we consider theorem proving problems specified by sets of first-order clauses that contain the axioms of a commutative ring with a unit element. Associative-commutative superposition forms the deductive core of our method, while a convergent rewrite system for commutative rings provides a starting point for more specialized inferences tailored to the given class of formulas. We adopt ideas from the Gr{\"o}bner basis method to show that many inferences of the superposition calculus are redundant. This result is obtained by the judicious application of the simplification techniques afforded by convergent rewriting and by a process called symmetrization that embeds inferences between single clauses and ring axioms.

Bachmair, L. and Ganzinger, H.

Abstract: We present an extended completion procedure with built-in theories defined by a collection of associativity and commutativity axioms and additional ground equations, and reformulate Buchberger's algorithm for constructing Gr\"obner 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 a wide class of correct completion procedures, among them Buchberger's original algorithm for polynomial rings over a field.

Bachmair, L. and Ganzinger, H.

Abstract: We propose inference systems based on ordered chaining and a concept of (global) redundancy for clauses and inferences for dealing with total orderings. A key to the practicality of chaining techniques is the extent to which so-called variable chainings can be restricted. We demonstrate that ordering restrictions and the rewrite techniques which account for their completeness considerably restrict variable chaining. For dense total orderings we show that the techniques for eliminating unshielded variables are admissible simplifications so that no variable chaining is needed at all. We also include equality by combining ordered chaining with superposition.

[an error occurred while processing this directive]