کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4662890 | 1633615 | 2016 | 11 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Tableau reductions: Towards an optimal decision procedure for the modal necessity
ترجمه فارسی عنوان
کاهش تابلو: به سوی یک روش تصمیم گیری بهینه برای ضرورت معین
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
منطق موجهات؛ روش تابلو؛ روش تصمیم گیری؛ سیستم های تابلو با پیشوند؛ مسئله مفروضات جهانی
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
چکیده انگلیسی
We present a new prefixed tableau system TKTK for verification of validity in modal logic KK. The system TKTK is deterministic, it uniquely generates exactly one proof tree for each clausal representation of formulas, and, moreover, it uses some syntactic reductions of prefixes. TKTK is defined in the original methodology of tableau systems, without any external technique such as backtracking, backjumping, etc. Since all the necessary bookkeeping is built into the rules, the system is not only a basis for a validity algorithm, but is itself a decision procedure. We present also a deterministic tableau decision procedure which is an extension of TKTK and can be used for the global assumptions problem.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Applied Logic - Volume 17, September 2016, Pages 14–24
Journal: Journal of Applied Logic - Volume 17, September 2016, Pages 14–24
نویسندگان
Joanna Golińska-Pilarek, Emilio Muñoz-Velasco, Angel Mora,