Tree automata help one to solve equational formulae in AC-theories

Abstract : In this paper we consider particular equational formulae where the equality = AC in the congruence induced by a set of associative-commutative axioms. The formulae we are interested in have the form t -AC t1 [??]. . . t -AC tn and are usually known as complement problems. To solve a complement problem is to find an instance of t which is not an instance of any ti modulo associativity-commutativity. We give a decision procedure based on tree automata which solves these formulae when all the ti's are linear. We show that this approach gives a decision of inductive reducibility modulo associativity and commutativity in the linear case and we give several extensions of this approach. Then, we define a new class of tree automata, called conditional tree automata which recognize sets of normalized terms (i.e. terms written as multisets) and where the application of a rule depends on the satisfiability of a formulae of Presburger's arithmetic. This class of tree automata allows one to solve non-linear complement problems when all occurences of a non-linear variable occur under the same node (in flattened terms). This solution also provides a decision of the inductive reducibility modulo associativity-commutativity in the same case.
Type de document :
Rapport
[Research Report] RR-2029, INRIA. 1993
Liste complète des métadonnées

https://hal.inria.fr/inria-00074642
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 15:58:30
Dernière modification le : samedi 17 septembre 2016 - 01:06:47
Document(s) archivé(s) le : mardi 12 avril 2011 - 17:56:55

Fichiers

Identifiants

  • HAL Id : inria-00074642, version 1

Collections

Citation

Denis Lugiez, Jean-Luc Moysset. Tree automata help one to solve equational formulae in AC-theories. [Research Report] RR-2029, INRIA. 1993. 〈inria-00074642〉

Partager

Métriques

Consultations de la notice

79

Téléchargements de fichiers

45