Reasoning with Global Assumptions in Arithmetic Modal Logics

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

Abstract

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.
 

Authors with CRIS profile

Related research project(s)

Involved external institutions

How to cite

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