EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies

DOI10.1007/978-3-540-73099-6_12zbMath1132.68731OpenAlexW1554599886MaRDI QIDQ5434485

Linh Anh Nguyen, Rajeev Goré

Publication date: 4 January 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73099-6_12

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Knowledge representation (68T30)

Related Items

ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching ⋮ Complexity of hybrid logics over transitive frames ⋮ Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse ⋮ Consequence-based and fixed-parameter tractable reasoning in description logics ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ Global Caching for Coalgebraic Description Logics ⋮ A Tableau Calculus for Regular Grammar Logics with Converse ⋮ Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs ⋮ ExpTime tableau decision procedures for regular grammar logics with converse ⋮ A new methodology for developing deduction methods ⋮ On the scalability of description logic instance retrieval

Uses Software

• LoTREC