|کد مقاله||کد نشریه||سال انتشار||مقاله انگلیسی||ترجمه فارسی||نسخه تمام متن|
|4662890||1345204||2016||11 صفحه PDF||ندارد||دانلود رایگان|
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.
Journal: Journal of Applied Logic - Volume 17, September 2016, Pages 14–24