Unification in a Class of Permutative Theories

  • Thierry Boy de la Tour
  • Mnacho Echenim
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Avenhaus, J., Plaisted, D.: General algorithms for permutations in equational inference. Journal of Automated Reasoning 26, 223–268 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Avenhaus, J.: Efficient algorithms for computing modulo permutation theories. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 415–429. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)Google Scholar
  4. 4.
    Boy de la Tour, T., Echenim, M.: NP-completeness results for deductive problems on stratified terms. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 315–329. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    de la Tour, T.B., Echenim, M.: On the complexity of deduction modulo leaf permutative equations. To appear in Journal of Automated Reasoning (2004)Google Scholar
  6. 6.
    de la Tour, T.B., Echenim, M.: Overlapping leaf permutative equations. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 430–444. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Garey, M., Johnson, D.S.: Computers and intractability: a guide to the theory of NP -completeness. Freeman, San Francisco (1979)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Thierry Boy de la Tour
    • 1
  • Mnacho Echenim
    • 1
  1. 1.LEIBNIZ laboratoryIMAG – CNRS, INPGGrenoble Cedex

Personalised recommendations