Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic SHI

TL;DR

This paper introduces the first cut-free tableau decision procedure for determining the satisfiability of knowledge bases in the expressive description logic SHI, achieving optimal exponential time complexity.

Contribution

It presents a novel cut-free tableau method that is the first to be optimal for SHI, extending previous approaches for less expressive logics.

Findings

First cut-free ExpTime tableau procedure for SHI

Achieves optimal decision complexity for satisfiability

Extends tableau methods to more expressive description logics

Abstract

We give the first cut-free ExpTime (optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHI, which extends the description logic ALC with transitive roles, inverse roles and role hierarchies.