Any ground associative-commutative theory has a finite canonical system

Abstract : We show that theories presented by a set of ground equations and with several associative-commutative symbols always admit a finite canonical system. In particular, the result is obtained through the construction of a reduction ordering which is AC-compatible and total on the set of congruence classes generated by the associativity and commutativity axioms. Such orderings are fundamental for deriving complete theorem proving strategies with built-in associative commutative unification.
Type de document :
Rapport
[Research Report] RR-1324, INRIA. 1990, pp.11
Liste complète des métadonnées

https://hal.inria.fr/inria-00075236
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 17:47:31
Dernière modification le : samedi 17 septembre 2016 - 01:06:51
Document(s) archivé(s) le : mardi 12 avril 2011 - 18:21:51

Fichiers

Identifiants

  • HAL Id : inria-00075236, version 1

Collections

Citation

Paliath Narendran, Michaël Rusinowitch. Any ground associative-commutative theory has a finite canonical system. [Research Report] RR-1324, INRIA. 1990, pp.11. 〈inria-00075236〉

Partager

Métriques

Consultations de la notice

123

Téléchargements de fichiers

60