It has been proposed in [1] 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 [1]; a subclass of flat equations has been considered only recently, in [2]. Our emphasis on group theoretic structures led us in [6] 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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
De La Tour, T. B., & Echenim, M. (2005). Unification in a class of permutative theories. In Lecture Notes in Computer Science (Vol. 3467, pp. 105–119). https://doi.org/10.1007/978-3-540-32033-3_9
Mendeley helps you to discover research relevant for your work.