Handling Nominals and Inverse Roles using Algebraic Reasoning
This work addresses a specific problem in description logic for researchers and practitioners in knowledge representation, with incremental improvements over existing methods.
The paper tackles the problem of deciding ontology consistency in SHOI by introducing a novel tableau calculus that uses algebraic reasoning to encode numerical restrictions into linear inequalities, which are solved with column generation and branch-and-price algorithms, resulting in preliminary experiments showing better performance compared to standard tableau methods.
This paper presents a novel SHOI tableau calculus which incorporates algebraic reasoning for deciding ontology consistency. Numerical restrictions imposed by nominals, existential and universal restrictions are encoded into a set of linear inequalities. Column generation and branch-and-price algorithms are used to solve these inequalities. Our preliminary experiments indicate that this calculus performs better on SHOI ontologies than standard tableau methods.