MPI-I-92-216
First-order theorem proving modulo equations
Wertz, Ulrich
April 1992, 108 pages.
.
Status: available - back from printing
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.
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-216
BibTeX
@TECHREPORT{Wertz-92-mpii216,
AUTHOR = {Wertz, Ulrich},
TITLE = {First-order theorem proving modulo equations},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-92-216},
MONTH = {April},
YEAR = {1992},
ISSN = {0946-011X},
}