کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423737 685285 2008 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Higher-Order Proof Construction Based on First-Order Narrowing
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Higher-Order Proof Construction Based on First-Order Narrowing
چکیده انگلیسی

We present the idea of using a proof checking algorithm for the purpose of automated proof construction. This is achieved by applying narrowing search on a proof checker expressed in a functional programming language. We focus on higher-order formalisms, such as logical frameworks, whereas the narrowing techniques we employ are first-order. An obvious advantage of this approach is that a single representation of the semantics can in principle be used for both proof checking and proof construction. The correctness of the search algorithm is consequently more or less trivially provided. The question is whether this representation of the search procedure allows a performance plausible for practical use. In order to achieve this, we add some features to the general narrowing search. We also present some small modifications which can be applied on a proof checker and which further improve the performance. We claim that the resulting proof search procedure is efficient enough for application in an interactive environment, where automation is used mostly on small subproofs.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 196, 22 January 2008, Pages 69-84