An ExpTime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic SHOQ

DOI10.3233/FI-2014-1133zbMATH Open1315.68231OpenAlexW1889795185MaRDI QIDQ5259302FDOQ5259302

Authors: Linh Anh Nguyen, Joanna Golińska-Pilarek 

Publication date: 26 June 2015

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/fi-2014-1133

Recommendations

• Algebraic tableau reasoning for the description logic \(\mathcal{SHOQ}\)
• Tableaux with Global Caching for Checking Satisfiability of a Knowledge Base in the Description Logic $\mathcal{SH}$
• scientific article; zbMATH DE number 1448975
• Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles
• EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies

zbMATH Keywords

description logicsautomated reasoningglobal state cachinginteger linear feasibility

Mathematics Subject Classification ID

Knowledge representation (68T30) Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35)

Cited In (5)

• Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
• Algebraic tableau reasoning for the description logic \(\mathcal{SHOQ}\)
• EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
• ExpTime tableaux with global caching for hybrid PDL
• Practical reasoning with qualified number restrictions: a hybrid Abox calculus for the description logic \({\mathcal{SHQ}}\).

This page was built for publication: An ExpTime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic SHOQ

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