Pay-as-you-go consequence-based reasoning for the description logic SROIQ

DOI10.1016/J.ARTINT.2021.103518MaRDI QIDQ2238693zbMATH OpenOpenAlexFDO

Authors David Tena Cucala, Bernardo Cuenca Grau, Ian Horrocks

Publication date 2 November 2021

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.artint.2021.103518

zbMATH Keywords

description logicsontologiesautomated reasoningknowledge representation and reasoning

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• Consequence-Based Reasoning for Description Logics with Disjunctions and Number Restrictions
• Pay-as-you-go description logic reasoning by coupling tableau and saturation procedures
• A resolution based description logic calculus
• Hypertableau reasoning for description logics
• Consequence-based and fixed-parameter tractable reasoning in description logics

Cites work

• scientific article; zbMATH DE number 1936671 (Why is no real title available?)
• scientific article; zbMATH DE number 1507191 (Why is no real title available?)
• scientific article; zbMATH DE number 1552532 (Why is no real title available?)
• scientific article; zbMATH DE number 3380160 (Why is no real title available?)
• scientific article; zbMATH DE number 2243392 (Why is no real title available?)
• A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$
• An ExpTime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic SHOQ
• An introduction to description logic
• Blocking and other enhancements for bottom-up model generation methods
• Computing small clause normal forms
• Consequence-Based Reasoning for Description Logics with Disjunctions and Number Restrictions
• Consequence-based and fixed-parameter tractable reasoning in description logics
• Decidability of SHIQ with complex role inclusion axioms
• Deciding expressive description logics in the framework of resolution
• First-order resolution methods for modal logics
• Hyper tableaux
• Hyperresolution for guarded formulae
• Hypertableau reasoning for description logics
• Modular reuse of ontologies: theory and practice
• Paramodulation-based theorem proving
• Resolution theorem proving
• Resolution-based methods for modal logics
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies
• Theorem proving with ordering and equality constrained clauses
• Using resolution for testing modal satisfiability and building models

Cited in

(3)

• Optimal fixed-premise repairs of \(\mathcal{E}\mathcal{L}\) TBoxes
• Pay-as-you-go description logic reasoning by coupling tableau and saturation procedures
• Consequence-based and fixed-parameter tractable reasoning in description logics

Describes a project that uses

Uses Software

• Pellet
• FaCT++
• Racer
• KAON2
• HermiT
• Konclude
• RacerPro
• Snorocket
• ELK

This page was built for publication: Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)

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