|Formal Methods and Deduction
|Prof. Dr. J. Avenhaus|
Publications of the AG Avenhaus in 2003
Computing in Theories Defined by Permutative Equations
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 E-equivalence 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 E-equivalence 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 E-equivalence
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 NP-complete. The
same holds for Ê replaced by E. We present
relatively efficient algorithms for these problems. Our algorithms
are based on knowledge from group theory.
As Postscript (gzipped) or as PDF.
- [AP01]: Avenhaus, J. ; Plaisted, D.:
General Algorithms for Permutations in Equational Inference,
J. Automated Reasoning 26, 2001, pp. 223-268.
Letzte Änderung: Wednesday, 26-Oct-05 08:59:20 GMT