Kupke C, Pattinson D, Schröder L (2015)
Publication Type: Conference contribution
Publication year: 2015
Publisher: Springer
City/Town: Berlin
Pages Range: 367--380
Conference Proceedings Title: Fundamentals of Computation Theory - 20th International Symposium, FCT 2015, Proceedings
Event location: Gdansk
DOI: 10.1007/978-3-319-22177-9_28
We establish a generic upper bound ExpTime for reasoning with
global assumptions in coalgebraic modal logics. Unlike earlier
results of this kind, we do not require a tractable set of tableau
rules for the instance logics, so that the result applies to wider
classes of logics. Examples are Presburger modal logic,
which extends graded modal logic with linear inequalities over
numbers of successors, and probabilistic modal logic with polynomial
inequalities over probabilities. We establish the theoretical upper
bound using a type elimination algorithm. We also provide a global
caching algorithm that offers potential for practical reasoning.
APA:
Kupke, C., Pattinson, D., & Schröder, L. (2015). Reasoning with Global Assumptions in Arithmetic Modal Logics. In Fundamentals of Computation Theory - 20th International Symposium, FCT 2015, Proceedings (pp. 367--380). Gdansk: Berlin: Springer.
MLA:
Kupke, Clemens, Dirk Pattinson, and Lutz Schröder. "Reasoning with Global Assumptions in Arithmetic Modal Logics." Proceedings of the Fundamentals of Computation Theory - 20th International Symposium, FCT 2015, Gdansk Berlin: Springer, 2015. 367--380.
BibTeX: Download