Conference contribution


Reasoning with Global Assumptions in Arithmetic Modal Logics


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

Event details
Event: Fundamentals of Computation Theory - 20th International Symposium, FCT 2015
Event location: Gdansk
Start date of the event: 17/08/2015
End date of the event: 19/08/2015

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.



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). 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
Share link
Last updated on 2017-03-23 at 01:37
PDF downloaded successfully