The application of goal-oriented heuristics for proving
equational theorems via the unfailing Knuth-Bendix
completion procedure
A case study: lattice ordered groups

Matthias Fuchs
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern, GERMANY
E-mail: fuchs@informatik.uni-kl.de


Abstract
In this report we present a case study of employing
goal-oriented heuristics when proving equational theorems with
the (unfailing) Knuth-Bendix completion procedure. The theorems
are taken from the domain of lattice ordered groups. It will be
demonstrated that goal-oriented (heuristic) criteria for
selecting the next critical pair can in many cases significantly
reduce the search effort and hence increase performance of the
proving system considerably. The heuristic, goal-oriented
criteria are on the one hand based on so-called `measures'
measuring occurrences and  nesting of function symbols, and on
the other hand based on matching subterms.  We also deal with
the property of goal-oriented heuristics to be particularly
helpful in certain stages of a proof. This fact can be
addressed by using them in a framework for distributed
(equational) theorem proving, namely the `teamwork-method'.

Keywords
Knuth-Bendix completion, equational theorem proving,
goal-orientation, distributed theorem proving

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1994/papers/
file: Fuchs.SR-94-02.ps.Z