ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
From MaRDI portal
Publication:352943
DOI10.1007/s10817-011-9243-0zbMath1361.68188OpenAlexW2077974960MaRDI QIDQ352943
Publication date: 5 July 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9243-0
modal logicdescription logicglobal caching complexity-optimal tableauxtableau-based decision procedures
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (10)
ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching ⋮ Reasoning with Global Assumptions in Arithmetic Modal Logics ⋮ Coalgebraic semantics of modal logics: an overview ⋮ An Experimental Evaluation of Global Caching for $\mathcal {ALC}$ (System Description) ⋮ Consequence-based and fixed-parameter tractable reasoning in description logics ⋮ Global Caching for Coalgebraic Description Logics ⋮ An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability ⋮ Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs ⋮ ExpTime tableaux with global caching for hybrid PDL ⋮ Description Logics
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
- ExpTime tableau decision procedures for regular grammar logics with converse
- Modal tableau calculi and interpolation
- A near-optimal method for reasoning about action
- Propositional dynamic logic of regular programs
- Cardinality restrictions on concepts
- EXPtime tableaux for ALC
- Converse-PDL with regular inclusion axioms: a framework for MAS logics
- Checking Consistency of an ABox w.r.t. Global Assumptions in PDL
- Tableaux with Global Caching for Checking Satisfiability of a Knowledge Base in the Description Logic $\mathcal{SH}$
- An Experimental Evaluation of Global Caching for $\mathcal {ALC}$ (System Description)
- Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
- Optimized Reasoning in Description Logics Using Hypertableaux
- Sound Global State Caching for ALC with Inverse Roles
- Optimizing description logic subsumption
- A description logic with transitive and inverse roles and role hierarchies
- Practical reasoning for very expressive description logics
- Efficient loop-check for backward proof search in some non-classical propositional logics
- A Tableau Calculus for Regular Grammar Logics with Converse
- An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
- Global Caching for Coalgebraic Description Logics
- Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
- An overview of tableau algorithms for description logics
- Analytic tableau systems and interpolation for the modal logics KB, KDB, K5, KD5
This page was built for publication: ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
