Congruence Closure modulo Associativity-Commutativity

Abstract : We introduce the notion of an associative-commutative congruence closure and show how such closures can be constructed via completion-like transition rules. This method is based on combining completion algorithms for theories over disjoint signatures to produce a convergent system over an extended signature. This approach can also be used to solve the word problem for ground AC-theories without using AC-simplification orderings. We also discuss transformation of a convergent system over an extended signature to a convergent system (modulo AC) over the original signature.
Type de document :
Communication dans un congrès
Kirchner, H. et Ringeissen, Ch. 3rd International Workshop on Frontiers of Combining Systems - FroCoS'2000, Mar 2000, Nancy, France, Springer Verlag, 1794, pp.242-256, 2000, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099214
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:51:48
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00099214, version 1

Collections

Citation

Leo Bachmair, I. V. Ramakrishnan, Ashish Tiwari, Laurent Vigneron. Congruence Closure modulo Associativity-Commutativity. Kirchner, H. et Ringeissen, Ch. 3rd International Workshop on Frontiers of Combining Systems - FroCoS'2000, Mar 2000, Nancy, France, Springer Verlag, 1794, pp.242-256, 2000, Lecture Notes in Computer Science. 〈inria-00099214〉

Partager

Métriques

Consultations de la notice

95