Someone Slept in My Bed! On the Entailment Problem for Conjunctive Queries with Safe Negation over DL-LiteCORE Knowledge Bases

Jul 16, 2026

Upload by Aria

The paper resolves a longstanding open problem by proving undecidability of query answering for conjunctive queries with safe negation over DL-LiteCORE knowledge bases. Given a DL-LiteCORE knowledge base ⟨TBox, ABox⟩ and a Boolean conjunctive query with safe negation ϕ, the work shows that determining whether O entails ϕ cannot be decided by any algorithm. The study develops technical preliminaries using first-order semantics, structure-as-fact views, and specialized query and model notions.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages8

Reading Time20 min

Abstract

Preliminaries

Structures and Relations

Queries

DL-LiteCORE and Query Entailment

Our Contribution

Theorem 1 (Undecidability)

Preliminaries (Part 2)

CQs with One Free Variable

Types of Vertices and the FREEZE Construct

Someone slept in my bed! On the entailment problem for conjunctive queries with safe negation over DL-Litecore knowledge bases Jerzy Marcinkowski University of Wrocław [jma@cs.uni.wroc.pl](jma@cs.uni.wroc.pl) Piotr Ostropolski-Nalewaja University of Wrocław [postropolski@cs.uni.wroc.pl](postropolski@cs.uni.wroc.pl) July 7, 2026 arXiv :2607 .05336v 1 [ cs .LO] 6 Jul 2026 Abstract We solve a long standing open problem, showing that the query answering for conjunctive queries with safe negation, over DL-LiteCORE knowledge bases, is undecidable. 1 Preliminaries. Part 1. We assume that the Reader is familiar with the standard notions regarding first-order logic (FOL) and its semantics. In particular, we use the terms signature, and atomic formula (or atom) in the standard sense. Fact is an atomic formula without variables (that is, only constants are allowed) . We assume that there exists some fixed infinite set C of constants. 1.1 Structures and Relations. The signatures we consider only comprise unary and binary predicates, so we think of relational structures (for short just structures) over such signatures as (coloured and labelled) graphs and, in consequence, we call elements of their domains vertices and sometimes we call the binary atoms edges. We find it notationally convenient to think that structures are just sets of facts. This means that the structures we consider never have isolated vertices and that only elements of C can serve as verticies. This can be assumed, for the purpose of this paper, without loss of generality. For a structure D by Dom (D) we denote the set of its vertices (that is the set of constants the facts of D mention) . Structure D1 is called a substructure of D2 if D1 ⊆ D2 (recall they are sets of facts) . If D is a structure and C ⊆ Dom (D) then the set: D [C] = {E(c, d) ∈ D ∶ c, d ∈ C} ∪ {A(c) ∈ D ∶ c ∈ C} is called an induced by C substructure of D. 1.2 Queries. A conjunctive query (CQ) is a FOL formula which is a conjunction of atoms preceded by existential quantifiers. A con- junctive query with safe negation (CQs ¬ ) is a CQ where negated atoms are allowed. It is however assumed, that every variable that appears in such query, must appear in some positive (that is non-negated) atom. A CQ (or a CQs ¬ ) is Boolean if all its variables are bound by existential quantifiers. We use the notations CQ (or CQs ¬ ) also to denote the respective classes of queries. For a Boolean ξ ∈ CQ ∪ CQs ¬ and a structure D by D ⊧ ξ we mean that ξ is true in D, in the usual FOL sense. Recall that if ξ ∈ CQ then D ⊧ ξ is equivalent to the existence of a mapping from (the variables of) ξ to D which is a homomorphism. If ξ ∈ CQs ¬ then, for D ⊧ ξ to hold, this homomorphism must satisfy some additional natural constraint, namely the image of a negated atom in ξ must not be an atom in D. We will call such mappings satisfying mappings. 1.3 The logic DL-LiteCORE and query entailment. The DL-Lite family of logics, and the logic DL-LiteCORE in particular, were introduced in [1] . Since our work is technical in nature, we will not discuss DL-Lite family in the full generality here, focusing instead on presenting the minimal set of definitions allowing us to formulate our results. A signature Σ comprising unary and binary predicates is assumed. A role is any binary relation over Σ or its inverse. A concept is any unary relation over Σ or any unary relation that can be defined as a projection of a role: for a role R, theset {x ∶ ∃y R(x, y)} is a concept, denoted as ∃R. A DL-Lite knowledge base O is a pair ⟨TBox, ABox⟩, where ABox is a structure (i.e. a set of facts) and TBox is the“domain knowledge” – a set of expressions involving roles and concepts. DL-LiteCORE is the least expressive of the logicsof family and only two forms of such expressions ale allowed in a DL-LiteCORE TBox, namely: () B ⊑ B ′ () B ⊑ ¬B ′ where B and B ′ are concepts. The semantics of the expressions is natural

FAQs

本文解决的核心开放问题是什么？

论文证明：在DL-LiteCORE知识库上，对带安全否定的合取查询（conjunctive queries with safe negation）的回答/蕴含判定是不可判定的，从而解决一个长期未决问题。

论文要判定的输入与问题形式是什么？

给定一个DL-LiteCORE知识库O以及一个带安全否定的布尔合取查询ϕ，询问O是否蕴含ϕ（即对所有满足O的结构ϕ都为真）。

什么是“安全否定”的合取查询？

在带安全否定的合取查询中允许出现被否定的原子，但要求查询里的每个变量都必须至少出现在某个正原子（非否定原子）中。

DL-LiteCORE知识库由哪些部分组成？

DL-LiteCORE知识库表示为⟨TBox, ABox⟩：ABox是由事实构成的结构，TBox给出涉及角色与概念的域知识，并只允许特定的概念包含/不相交形式。

Jul 16, 2026

Upload by Aria