کد مقاله کد نشریه سال انتشار مقاله انگلیسی ترجمه فارسی نسخه تمام متن
4662890 1345204 2016 11 صفحه PDF ندارد دانلود رایگان
عنوان انگلیسی مقاله
Tableau reductions: Towards an optimal decision procedure for the modal necessity ☆
ترجمه فارسی عنوان
کاهش تابلو: به سوی یک روش تصمیم گیری بهینه برای ضرورت معین
کلمات کلیدی
منطق موجهات؛ روش تابلو؛ روش تصمیم گیری؛ سیستم های تابلو با پیشوند؛ مسئله مفروضات جهانی
Modal logics; Tableau methods; Decision procedures; Prefixed tableau systems; Global assumptions problem
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

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
نویسندگان
, , ,