Research Group Logo CS Dept.
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.


Impressum AG Formale Methoden und Deduktion Fachbereich Informatik Technische Universität Kaiserslautern Valid HTML 4.01!

Letzte Änderung: Wednesday, 26-Oct-05 08:59:20 GMT