کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4661709 1633452 2015 36 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Inductive theorem proving based on tree grammars
ترجمه فارسی عنوان
بر اساس گرامرهای درخت اثبات قضیه هندسی
کلمات کلیدی
ترجمه چکیده
القایی نقش کلیدی در استدلال در بسیاری از زمینه های ریاضیات و علوم رایانه ای دارد. یک مشکل مرکزی در اتوماسیون اثبات با القاء، طبیعت غیر تحلیلی غیرقابل تحمل است. در این مقاله الگوریتمی برای اثبات اظهارات جهانی توسط القایی ارائه شده است که این مسئله را به دو مرحله جدا می کند. مرحله اول شامل تجزیه و تحلیل ساختاری از شرایط شاهد نمونه موارد بیانیه جهانی است. نتیجه چنین تحلیلی، یک گرامر درخت است که یک مسئله متحد سازی بدون رقم را ایجاد می کند که در مرحله دوم حل شده است. هر راه حل برای این مشکل، یک الگوی القایی است. استدلال ها و تکنیک های مورد استفاده در این مقاله به شدت از یک مکاتبات میان گرامرهای درختی و اثبات هایی که در حال حاضر به طور موفقیت آمیزی به تولید نسبی کاهش غیر تحلیلی در تنظیم منطق خالص مرتبه اول اعمال می شود، بهره می گیرند.
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
پیش نمایش مقاله
بر اساس گرامرهای درخت اثبات قضیه هندسی
چکیده انگلیسی
Induction plays a key role in reasoning in many areas of mathematics and computer science. A central problem in the automation of proof by induction is the non-analytic nature of induction invariants. In this paper we present an algorithm for proving universal statements by induction that separates this problem into two phases. The first phase consists of a structural analysis of witness terms of instances of the universal statement. The result of such an analysis is a tree grammar which induces a quantifier-free unification problem which is solved in the second phase. Each solution to this problem is an induction invariant. The arguments and techniques used in this paper heavily exploit a correspondence between tree grammars and proofs already applied successfully to the generation of non-analytic cuts in the setting of pure first-order logic.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 166, Issue 6, June 2015, Pages 665-700
نویسندگان
, ,