Help Privacy Policy Disclaimer
  Advanced SearchBrowse





First-order theorem proving modulo equations


Wertz,  Ulrich
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (public)

(Any fulltext), 72MB

Supplementary Material (public)
There is no public supplementary material available

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

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B729-0
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.