Non-distributive description logic

TL;DR

This paper introduces LE-ALC, a non-distributive generalization of ALC based on lattice logic, enabling formal description of databases with objects and features using FCA, with efficient consistency checking algorithms.

Contribution

It defines LE-ALC, a novel non-distributive description logic, and provides a tableaux algorithm with polynomial-time consistency checking for certain TBoxes.

Findings

Consistency checking in LE-ALC is in PTIME for acyclic TBoxes.

LE-ALC extends ALC by incorporating non-distributive lattice logic.

The tableaux algorithm is sound, complete, and terminates for the specified class of TBoxes.

Abstract

We define LE-ALC, a generalization of the description logic ALC based on the propositional logic of general (i.e. not necessarily distributive) lattices, and semantically interpreted on relational structures based on formal contexts from Formal Concept Analysis (FCA). The description logic LE-ALC allows us to formally describe databases with objects, features, and formal concepts, represented according to FCA as Galois-stable sets of objects and features. We describe ABoxes and TBoxes in LE-ALC, provide a tableaux algorithm for checking the consistency of LE-ALC knowledge bases with acyclic TBoxes, and show its termination, soundness and completeness. Interestingly, consistency checking for LE-ALC is in PTIME for acyclic and completely unravelled TBoxes, while the analogous problem in the classical ALC setting is PSPACE-complete.