We propose a notion of focusing for nested sequent calculi for modal logics which brings down the complexity of proof search to that of the corresponding sequent calculi. The resulting systems are amenable to specifications in linear logic. Examples include modal logic K, a simply dependent bimodal logic and the standard non-normal modal logics. As byproduct we obtain the first nested sequent calculi for the considered non-normal modal logics.
CITATION STYLE
Lellmann, B., & Pimentel, E. (2015). Proof search in nested sequent calculi. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9450, pp. 558–574). Springer Verlag. https://doi.org/10.1007/978-3-662-48899-7_39
Mendeley helps you to discover research relevant for your work.