Skip navigation
Skip navigation

Reasoning with Global Assumptions in Arithmetic Modal Logics

Kupke, Clemens; Pattinson, Dirk; Schroder, Lutz

Description

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...[Show more]

dc.contributor.authorKupke, Clemens
dc.contributor.authorPattinson, Dirk
dc.contributor.authorSchroder, Lutz
dc.date.accessioned2016-02-24T22:42:00Z
dc.identifier.issn0302-9743
dc.identifier.urihttp://hdl.handle.net/1885/98894
dc.description.abstractWe 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.
dc.publisherSpringer
dc.sourceLecture Notes in Computer Science (LNCS)
dc.titleReasoning with Global Assumptions in Arithmetic Modal Logics
dc.typeJournal article
local.description.notesImported from ARIES
local.identifier.citationvolume9210 Fundamentals of Computation Theory
dc.date.issued2015
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.ariespublicationu4334215xPUB1544
local.type.statusPublished Version
local.contributor.affiliationKupke, Clemens, University of Strathclyde
local.contributor.affiliationPattinson, Dirk, College of Engineering and Computer Science, ANU
local.contributor.affiliationSchroder, Lutz, Friedrich-Alexander Universitat
local.description.embargo2037-12-31
local.bibliographicCitation.startpage367
local.bibliographicCitation.lastpage380
local.identifier.doi10.1007/978-3-319-22177-9_28
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
dc.date.updated2016-06-14T09:03:38Z
local.identifier.scopusID2-s2.0-84943641178
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Kupke_Reasoning_with_Global_2015.pdf231.35 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator