@inproceedings{3ea83fba9cbe4787a1048e38caef7198,
title = "A modal-layered resolution calculus for K",
abstract = "Resolution-based provers for multimodal normal logics require pruning of the search space for a proof in order to deal with the inherent intractability of the satisfiability problem for such logics. We present a clausal modal-layered hyper-resolution calculus for the basic multimodal logic, which divides the clause set according to the modal depth at which clauses occur. We show that the calculus is complete for the logics being considered. We also show that the calculus can be combined with other strategies. In particular, we discuss the completeness of combining modal layering and negative resolution. In addition, we present an incompleteness result for modal layering together with ordered resolution.",
author = "C. Nalon and U. Hustadt and C. Dixon",
year = "2015",
doi = "10.1007/978-3-319-24312-2\_13",
language = "English",
isbn = "978-3-319-24311-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature",
pages = "185--200",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods",
address = "United States",
note = "TABLEAUX: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods : 24th International Conference, TABLEAUX 2015 ; Conference date: 21-09-2015 Through 24-09-2015",
}