An alternative for handling AC

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

Abstract
A method for efficiently handling associativity and commutativity (AC) in
implementations of (equational) theorem provers without incorporating AC as an
underlying theory will be presented. The key of substantial efficiency gains
resides in a more suitable representation of permutation-equations (such as
f(x,f(y,z))=f(y,f(z,x)) for instance). By representing these permutation-
equations through permutations in the mathematical sense (i.e. bijective
functions s:{1,..,n}->{1,..,n}), and by applying adapted and specialized
inference rules, we can cope more appropriately with the fact that
permutation-equations are playing a particular role. Moreover, a number of
restrictions concerning application and generation of permutation-equations
can be found that would not be possible in this extent when treating
permutation-equations just like any other equation. Thus, further improvements
in efficiency can be achieved.

Keywords
theorem proving, associative and commutative functions

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-03.ps.Z