کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4950015 | 1440354 | 2017 | 19 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
From Cut-free Calculi to Automated Deduction: The Case of Bounded Contraction
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
The addition of the bounded contraction rules to Full Lambek Calculus with exchange and weakening (FLew) gives rise to serious complications for proof search. For example, adding to FLew a naive version of these rules brakes cut-admissibility. Although this can be avoided by refining these rules, in this work we show that even “good” proof systems for FLew plus bounded contraction do not necessarily lead to good implementations. In order to solve this problem, we propose an extension of the lazy splitting methodology to bounded contractions, showing how to transform our focused, cut-free sequent calculus into a terminating theorem prover. Our system is used to show that the decision problem for FLew with bounded contraction is in EXPTIME.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 332, 11 June 2017, Pages 75-93
Journal: Electronic Notes in Theoretical Computer Science - Volume 332, 11 June 2017, Pages 75-93
نویسندگان
Agata Ciabattoni, Björn Lellmann, Carlos Olarte, Elaine Pimentel,