Item

Abstract

We present refutationally complete calculi for first-order clauses with equality. General paramodulation calculi cannot efficiently deal with equations such as associativity and commutativity axioms. Therefore we will separate a set of equations (called {$E$}-equations) from a specification and give them a special treatment, avoiding paramodulations with {$E$}-equations but using {$E$}-unification for the calculi. Techniques for handling such {$E$}-equations known in the context of purely equational specifications (e.g. computing critical pairs with {$E$}-equations or introducing extended rules) can be adopted for specifications with full first-order clauses. Methods for proving completeness results are based on the construction of equality Herbrand interpretations for consistent sets of clauses. These interpretations are presented as a set of ground rewrite rules and a set of ground instances of {$E$}-equations forming a Church-Rosser system. The construction of such Church-Rosser systems differs from constructions without considering {$E$}-equations in a non-trivial way. {$E$}-equations influence the ordering involved. Methods for defining {$E$}-compatible orderings are discussed. All these aspects are considered especially for the case that {$E$} is a set of associativity and commutativity axioms for some operator symbols (then called {$AC$}-operators). Some techniques and notions specific to specifications with {$AC$}-operators are included.