Research Group


Formal Methods and Deduction 
Prof. Dr. J. Avenhaus 
Publications of the AG Avenhaus in 2003

Computing in Theories Defined by Permutative Equations
Abstract:
In automated deduction it is sometimes helpful to compute modulo a
set E of equations. In this paper we consider the case where
E consists of permutative equations only. In this case it is
not easy to represent any Eequivalence class
[t]_{E} by just one representative and
to compute with these representatives efficiently. Therefore, in
[AP01] a method is presented to modify E to Ê
and to approximate the Eequivalence classes
[t]_{E} by Êequivalence
classes [t]_{Ê} for
”stratified“ terms t. Then one can compute
relatively efficiently with these Êequivalence
classes. In this paper we improve algorithms given in [AP01].
Provided that E satisfies some conditions, one can avoid the
construction of [AP01] and compute with the Eequivalence
class directly. Our results apply to this case, too.
If E is allowed to be part of the input then even testing
Êequality is at least as hard as testing for graph
isomorphism. For a fixed set E we present a polynomial time
algorithm for testing Êequality. Testing matchability
and unifiability modulo Ê is NPcomplete. The
same holds for Ê replaced by E. We present
relatively efficient algorithms for these problems. Our algorithms
are based on knowledge from group theory.
Download:
As Postscript (gzipped) or as PDF.
References:
 [AP01]: Avenhaus, J. ; Plaisted, D.:
General Algorithms for Permutations in Equational Inference,
J. Automated Reasoning 26, 2001, pp. 223268.
Letzte Änderung: Wednesday, 26Oct05 08:59:20 GMT
wwwaven@informatik.unikl.de