The Complexity of Satisfiability for Sub-Boolean Fragments of ALC

TL;DR

This paper investigates the computational complexity of concept satisfiability in various Boolean-restricted fragments of the description logic ALC, identifying which restrictions lead to tractable or intractable reasoning problems.

Contribution

It systematically analyzes the complexity of concept satisfiability under Boolean operator restrictions in ALC fragments, providing a comprehensive classification.

Findings

Identifies tractable and intractable Boolean restrictions in ALC

Establishes complexity boundaries for ALC fragments with axioms

Provides a systematic framework for understanding Boolean operator impacts

Abstract

The standard reasoning problem, concept satisfiability, in the basic description logic ALC is PSPACE-complete, and it is EXPTIME-complete in the presence of unrestricted axioms. Several fragments of ALC, notably logics in the FL, EL, and DL-Lite family, have an easier satisfiability problem; sometimes it is even tractable. All these fragments restrict the use of Boolean operators in one way or another. We look at systematic and more general restrictions of the Boolean operators and establish the complexity of the concept satisfiability problem in the presence of axioms. We separate tractable from intractable cases.