Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics

DOI10.1145/3501300zbMATH Open1502.68285arXiv2009.00971OpenAlexW3081939111WikidataQ114613905 ScholiaQ114613905MaRDI QIDQ5034233FDOQ5034233

Lutz Schröder, Clemens Kupke, Dirk Pattinson

Publication date: 24 February 2022

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does 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 potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka's linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e. in coalgebraic hybrid logic.

Full work available at URL: https://arxiv.org/abs/2009.00971

zbMATH Keywords

coalgebraic logicdescription logicshybrid logicprobabilistic modal logicglobal cachingTBoxesglobal assumptionsPresburger modal logic

Mathematics Subject Classification ID

Knowledge representation (68T30) Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27)

Cited In (3)

• How to tell easy from hard: complexities of conjunctive query entailment in extensions of \(\mathcal{ALC}\)
• Coalgebraic satisfiability checking for arithmetic \(\mu\)-calculi
• COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Coalgebraic Modal Logic Beyond Sets 👍 👎
• Coalgebraic modal logic: soundness, completeness and decidability of local consequence 👍 👎
• Coalgebraic semantics of modal logics: an overview 👍 👎
• Specifying coalgebras with modal logic 👍 👎
• Coalgebraic modal logic of finite rank 👍 👎
• Reasoning with Global Assumptions in Arithmetic Modal Logics 👍 👎
• Coalgebras and modal expansions of logics 👍 👎
• Coalgebraic Modal Logic in CoCasl 👍 👎

This page was built for publication: Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5034233)