کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
401460 | 675361 | 2008 | 16 صفحه PDF | دانلود رایگان |

We study matching in flat theories both from theoretical and practical points of view. A flat theory is defined by the axiom that indicates that nested occurrences of the function symbol f can be flattened out. From the theoretical side, we design a procedure to solve a system of flat matching equations and prove its soundness, completeness, and minimality. The minimal complete set of matchers for such a system can be infinite. The procedure enumerates this set and stops if it is finite. We identify a class of problems on which the procedure stops. From the practical point of view, we look into restrictions of the procedure that give an incomplete terminating algorithm. From this perspective, we give a set of rules that, in our opinion, describes the precise semantics for the flat matching algorithm implemented in the Mathematica system.
Journal: Journal of Symbolic Computation - Volume 43, Issue 12, December 2008, Pages 858-873