Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.
|Title of host publication||Proceedings of Advances in Modal Logic 2016|
|Editors||Lev Beklemishev, Stéphane Demri, András Máté|
|Publication status||Published - 2016|
|Event||Advances in Modal Logic 2016 - Eotvos University, Budapest, Hungary|
Duration: 30 Aug 2016 → 2 Sep 2016
http://phil.elte.hu/aiml2016/ (Link to Conference)
|Conference||Advances in Modal Logic 2016|
|Period||30/08/2016 → 02/09/2016|
Jørgensen, K. F., Blackburn, P. R., Bolander, T., & Braüner, T. (2016). Synthetic Completeness Proofs for Seligman-style Tableau Systems. In L. Beklemishev, S. Demri, & A. Máté (Eds.), Proceedings of Advances in Modal Logic 2016 (Vol. 11, pp. 302-321). College Publications.