# Finite Satisfiability of Unary Negation Fragment with Transitivity

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Sep 2018.

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

- [A Review of SHACL: From Data Validation to Schema Reasoning for RDF Graphs](https://mlsanity.com/paper/2112.01441/) (2021)
- [Satisfiability and Containment of Recursive SHACL](https://mlsanity.com/paper/2108.13063/) (2021)
- [Finite Entailment of UCRPQs over ALC Ontologies](https://mlsanity.com/paper/2204.14261/) (2022)

## Abstract (arXiv)

We show that the finite satisfiability problem for the unary negation fragment with arbitrary number of transitive relations is decidable and 2-ExpTime-complete. Our result actually holds for a more general setting in which one can require that some binary symbols are interpreted as arbitrary transitive relations, some as partial orders and some as equivalences. We also consider finite satisfiability of various extensions of our primary logic, in particular capturing the concepts of nominals and role hierarchies known from description logic. As the unary negation fragment can express unions of conjunctive queries our results have interesting implications for the problem of finite query answering, both in the classical scenario and in the description logics setting.