Finite Satisfiability of Unary Negation Fragment with Transitivity

TL;DR

This paper proves that the finite satisfiability problem for the unary negation fragment with transitive, partial order, and equivalence relations is decidable and 2-ExpTime-complete, with implications for query answering.

Contribution

It establishes decidability and complexity results for the finite satisfiability of an extended unary negation logic with various relational features.

Findings

Finite satisfiability is decidable for the logic with transitive, partial order, and equivalence relations.

The problem is 2-ExpTime-complete.

Results extend to logic variants with nominals and role hierarchies.

Abstract

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.