کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
10330950 686395 2005 39 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Source-tracking unification
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Source-tracking unification
چکیده انگلیسی
We propose a path-based framework for deriving and simplifying source-tracking information for first-order term unification in the empty theory. Such a framework is useful for diagnosing unification-based systems, including debugging of type errors in programs and the generation of success and failure proofs in logic programming. The objects of source-tracking are deductions in the logic of term unification. The semantics of deductions are paths over a unification graph whose labels form the suffix language of a semi-Dyck set. Based on this idea of unification paths, two algorithms for generating proofs are presented: the first uses context-free labeled shortest-path algorithms to generate optimal (shortest) proofs in time O (n3) for a fixed signature, 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.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 201, Issue 2, 15 September 2005, Pages 121-159
نویسندگان
, ,