کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
433680 | 689600 | 2016 | 22 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
On natural deduction in classical first-order logic: Curry–Howard correspondence, strong normalization and Herbrand's theorem
ترجمه فارسی عنوان
در کسر طبیعی در منطق مرتبه اول کلاسیک: مکاتبات کاریانی، نرمال شدن قوی و قضیه هربراند
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
We present a new Curry–Howard correspondence for classical first-order natural deduction. We add to the lambda calculus an operator which represents, from the viewpoint of programming, a mechanism for raising and catching multiple exceptions, and from the viewpoint of logic, the excluded middle over arbitrary prenex formulas. The machinery will allow to extend the idea of learning – originally developed in Arithmetic – to pure logic. We prove that our typed calculus is strongly normalizing and show that proof terms for simply existential statements reduce to a list of individual terms forming an Herbrand disjunction. A by-product of our approach is a natural-deduction proof and a computational interpretation of Herbrand's Theorem.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 625, 25 April 2016, Pages 125–146
Journal: Theoretical Computer Science - Volume 625, 25 April 2016, Pages 125–146
نویسندگان
Federico Aschieri, Margherita Zorzi,