Reasoning with Global Assumptions in Arithmetic Modal Logics

Conference contribution


Publication Details

Author(s): Kupke C, Pattinson D, Schröder L
Publisher: Springer
Publishing place: Berlin
Publication year: 2015
Conference Proceedings Title: Fundamentals of Computation Theory - 20th International Symposium, FCT 2015, Proceedings
Pages range: 367--380


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.

 



FAU Authors / FAU Editors

Schröder, Lutz Prof. Dr.
Lehrstuhl für Informatik 8 (Theoretische Informatik)


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: 

Last updated on 2018-19-04 at 03:20