# Description Logic Knowledge and Action Bases

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Feb 2014.

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

- [Towards Ontology-Mediated Planning with OWL DL Ontologies (Extended Version)](https://mlsanity.com/paper/2308.08200/) (2023)
- [Current and Future Challenges in Knowledge Representation and Reasoning](https://mlsanity.com/paper/2308.04161/) (2023)
- [Reasoning about actions with EL ontologies with temporal answer sets](https://mlsanity.com/paper/2107.08403/) (2021)
- [SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version)](https://mlsanity.com/paper/2108.12330/) (2021)
- [Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)](https://mlsanity.com/paper/2208.06377/) (2022)
- [A Strategy for Implementing description Temporal Dynamic Algorithms in Dynamic Knowledge Graphs by SPIN](https://mlsanity.com/paper/2401.07890/) (2024)
- [Planning with OWL-DL Ontologies (Extended Version)](https://mlsanity.com/paper/2408.07544/) (2024)
- [RDFdL: Integrating RDF with Differential Dynamic Logic](https://mlsanity.com/paper/2608.18165/) (2026)

## Abstract (arXiv)

Description logic Knowledge and Action Bases (KAB) are a mechanism for providing both a semantically rich representation of the information on the domain of interest in terms of a description logic knowledge base and actions to change such information over time, possibly introducing new objects. We resort to a variant of DL-Lite where the unique name assumption is not enforced and where equality between objects may be asserted and inferred. Actions are specified as sets of conditional effects, where conditions are based on epistemic queries over the knowledge base (TBox and ABox), and effects are expressed in terms of new ABoxes. In this setting, we address verification of temporal properties expressed in a variant of first-order mu-calculus with quantification across states. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of weak acyclicity in data exchange.