Deduction and Unification in Permutative Theories

Many state-of-the art theorem provers can perform deductions modulo an equational theory, by considering equivalence classes of terms, instead of ordinary terms. Most of the existing approaches focus on determining new and more efficient techniques to perform deduction modulo only one theory, such as associativity and commutativity. A more general research direction is to try to determine efficient techniques that could be used to treat not one specific theory, but an entire class of equational theories. If such techniques were to be integrated in a theorem prover, it would be possible to solve several problems very efficiently without any prior human intervention.

In this presentation, we will consider the class of leaf-permutative theories. These theories enjoy several regularity properties that make it possible to use efficient techniques from computational group theory to deal with them. The use of group-theoretic techniques is nontrivial, and I will show that it can be done quite elegantly thanks to the conceps of stratified term-graphs. There are several problems any theorem prover dealing with leaf-permutative theories has to solve, and thanks to our formalism, we can prove that these problems are all NP-hard. Finally, I will present a subclass of leaf-permutative theories, the so-called unify-stable theories, that enjoy better complexity properties, and I will show that we can solve any unification problem modulo such a theory.