# Efficient Computation of General Modules for ALC Ontologies (Extended Version)

arXiv: https://arxiv.org/abs/2305.09503 · HTML: https://mlsanity.com/paper/2305.09503/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 1 of its 46 references that are in the map.
- First posted on arXiv 16 May 2023.

## Builds on (most cited first, 1 of 1)

- [Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)](https://mlsanity.com/paper/2004.08311/) (2020)

## Built on by (most cited first, 4 of 4)

- [TransBox: EL++-closed Ontology Embedding](https://mlsanity.com/paper/2410.14571/) (2024)
- [Large Language Model for OWL Proofs](https://mlsanity.com/paper/2601.12444/) (2026)
- [Interpolation in Knowledge Representation](https://mlsanity.com/paper/2512.08833/) (2025)
- [Rethinking Explanations: Formalizing Contrast in Description Logics](https://mlsanity.com/paper/2605.01442/) (2026)

## Abstract (arXiv)

We present a method for extracting general modules for ontologies formulated in the description logic ALC. A module for an ontology is an ideally substantially smaller ontology that preserves all entailments for a user-specified set of terms. As such, it has applications such as ontology reuse and ontology analysis. Different from classical modules, general modules may use axioms not explicitly present in the input ontology, which allows for additional conciseness. So far, general modules have only been investigated for lightweight description logics. We present the first work that considers the more expressive description logic ALC. In particular, our contribution is a new method based on uniform interpolation supported by some new theoretical results. Our evaluation indicates that our general modules are often smaller than classical modules and uniform interpolants computed by the state-of-the-art, and compared with uniform interpolants, can be computed in a significantly shorter time. Moreover, our method can be used for, and in fact improves, the computation of uniform interpolants and classical modules.