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

DOI10.3233/FI-2014-1133MaRDI QIDQ5259302zbMATH OpenOpenAlexFDO

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

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)

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

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)