Tableau reductions: Towards an optimal decision procedure for the modal necessity

We present a new prefixed tableau system TK for verification of validity in modal logic K. The system TK is deterministic, it uniquely generates exactly one proof tree for each clausal representation of formulas, and, moreover, it uses some syntactic reductions of prefixes. TK is defined in the orig...

Full description

Saved in:
Bibliographic Details
Published in:Journal of applied logic 2016-09, Vol.17, p.14-24
Main Authors: Golińska-Pilarek, Joanna, Muñoz-Velasco, Emilio, Mora, Angel
Format: Article
Language:English
Subjects:
Decision procedures
Global assumptions problem
Modal logics
Prefixed tableau systems
Tableau methods
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a new prefixed tableau system TK for verification of validity in modal logic K. The system TK is deterministic, it uniquely generates exactly one proof tree for each clausal representation of formulas, and, moreover, it uses some syntactic reductions of prefixes. TK 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 TK and can be used for the global assumptions problem.
ISSN:1570-8683
1570-8691
DOI:10.1016/j.jal.2015.09.005