Research Group
Formal Methods and Deduction
Prof. Dr. J. Avenhaus

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 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.

Download:

References:

• [AP01]: Avenhaus, J. ; Plaisted, D.: General Algorithms for Permutations in Equational Inference, J. Automated Reasoning 26, 2001, pp. 223-268.

Impressum

AG Formale Methoden und Deduktion

Fachbereich Informatik

Technische Universität Kaiserslautern