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 (restricted access)
There are currently no full texts shared for your IP range.
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: https://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.