HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 3:58:30 PM
Last modification on : Friday, February 4, 2022 - 3:16:48 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 5:56:55 PM


  • HAL Id : inria-00074642, version 1



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



Record views


Files downloads