Source-Tracking Unification

12 years 5 months ago
Source-Tracking Unification
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...
Venkatesh Choppella, Christopher T. Haynes
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where CADE
Authors Venkatesh Choppella, Christopher T. Haynes
Comments (0)