We propose a practical path-based framework for deriving and simplifying source-tracking information for term unification in the empty theory. Such a framework is useful for debugging unification-based systems, including the diagnosis of ill-typed programs and the generation of success and failure proofs in logic programming. The objects of source-tracking are deductions in the logic of unification. The semantics of deductions are paths over a unification graph whose labels form the language of suffixes of a semi-Dyck set. Based on this framework, two algorithms for generating proofs are presented: the first uses context-free shortest-path algorithms to generate optimal (shortest) proofs in time O(n3), where n is the number of vertices of the unification graph. The second algorithm integrates easily with standard unification algorithms, entailing an overhead of only a constant factor, but generates non-optimal proofs. These non-optimal proofs may be further simplified by group rewrite rules.
CITATION STYLE
Choppella, V., & Haynes, C. T. (2003). Source-tracking unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 458–472). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_39
Mendeley helps you to discover research relevant for your work.