Handling Nominals and Inverse Roles using Algebraic Reasoning

TL;DR

This paper introduces an algebraic reasoning-based tableau calculus for SHOI ontologies, encoding restrictions as linear inequalities and solving them with advanced algorithms, improving performance over standard methods.

Contribution

It presents a novel SHOI tableau calculus that integrates algebraic reasoning and advanced algorithms to enhance ontology consistency checking.

Findings

Better performance on SHOI ontologies compared to standard tableau methods

Effective encoding of restrictions into linear inequalities

Use of column generation and branch-and-price algorithms

Abstract

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.