An ExpTime Tableau Method for Dealing with Nominals and Qualified Number Restrictions in Deciding the Description Logic SHOQ

DOI10.3233/FI-2014-1133zbMath1315.68231OpenAlexW1889795185MaRDI QIDQ5259302

Joanna Golińska-Pilarek, Linh Anh Nguyen

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

automated reasoningdescription logicsglobal state cachinginteger linear feasibility

Mathematics Subject Classification ID

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

Related Items (2)

Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) ⋮ ExpTime tableaux with global caching for hybrid PDL

This page was built for publication: An ExpTime Tableau Method for Dealing with Nominals and Qualified Number Restrictions in Deciding the Description Logic SHOQ