Unification in a Class of Permutative Theories
It has been proposed in  to perform deduction modulo leaf permutative theories, which are notoriously hard to handle directly in equational theorem proving. But unification modulo such theories is a difficult task, not tackled in ; a subclass of flat equations has been considered only recently, in . Our emphasis on group theoretic structures led us in  to the definition of a more general subclass of leaf permutative theories, the unify-stable theories. They have good semantic and algorithmic properties, which we use here to design a complete unification algorithm.
Unable to display preview. Download preview PDF.