Tableau systems for deontic action logics based on finite Boolean algebras, and their complexity (Q526730)

The author examines a deontic logic of actions known as DAL, which was devised by \textit{K. Segerberg} [Stud. Log. 41, 269--282 (1982; Zbl 0537.03018)] and subsequently studied and varied in papers by \textit{P. F. Castro} and \textit{T. S. E. Maibaum} [Lect. Notes Comput. Sci. 5076, 34--48 (2008; Zbl 1143.68595); J. Appl. Log. 7, No. 4, 441--466 (2009; Zbl 1193.03060)] and most recently by \textit{R. Trypuz} and \textit{P. Kulicki} [J. Log. Comput. 25, No. 5, 1241--1260 (2015; Zbl 1336.03027)]. The focus is on computational aspects of the system. The author gives tableau characterizations for DAL and its extant variants, and obtains results on the computational complexity of their satisfiability problems.