# Item

ITEM ACTIONSEXPORT

Released

Report

#### First-order theorem proving modulo equations

##### MPS-Authors

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

MPI-I-92-216.pdf

(Any fulltext), 72MB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Wertz, U.(1992). *First-order theorem proving modulo equations*
(MPI-I-92-216). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B729-0

##### 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.