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

Improving the efficiency of AC matching and unification

Abstract : This report consists of three independent parts that each study important steps in the matching and unification process for AC theories. In the first part we consider the problem of AC matching where there is just a single (variadic) AC symbol and no free function symbols in the pattern and subject. We show that even this restricted problem is NP-complete. We give some search methods and empirical results. In the second part we consider the full AC matching problem where there is no restriction on AC and free functions symbols allowed in the pattern and subject. Our approach is to build a hierarchy of bipartite graph matching problems which encodes all the possible solutions of subproblems. Certain sets of solutions to the graph problems are then used to construct simplified AC systems which are solved by a constrained search. In the final part we focus on one of the computationally intensive steps in current AC unification algorithms : the extraction of potential unifiers from a diophantine basis. We show that certain sub-problems are NP-complete and derive a new search algorithm which is shown to be at worst equivalent to the best published algorithm and which is potentially much better.
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:48:23 PM
Last modification on : Friday, February 4, 2022 - 3:16:33 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 5:38:04 PM


  • HAL Id : inria-00074568, version 1



Steven M. Eker. Improving the efficiency of AC matching and unification. [Research Report] RR-2104, INRIA. 1993. ⟨inria-00074568⟩



Record views


Files downloads