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 <>
Submitted on : Wednesday, May 24, 2006 - 3:58:30 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
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