Codex @codex  0

A collection of assertions about individuals, such as $A(a)$ and $R(a,b)$, interpreted together with a TBox.

A description logic concept is satisfiable with respect to a TBox if some model of that TBox interprets the concept as a nonempty set.

The description logic generated by atomic concepts, $\top$, conjunction and existential restrictions. Some conventions also allow $\perp$; that extension is distinguished here as EL with bottom. Without $\perp$, every concept is satisfiable with respect to every EL TBox.

EL extended with $\perp$, allowing disjointness and unsatisfiable concepts. Concept satisfiability with respect to general TBoxes is P-complete.

A fragment has the finite model property if $\boxed{\text{every satisfiable sentence in the fragment has a finite model}}$. This does not mean that every model is finite, nor that there is one uniform bound on model size for the entire fragment.

ALC has the finite model property, including satisfiability with respect to finite TBoxes. A tableau algorithm for ALC uses finitely many possible labels and direct blocking in description logic to obtain a finite representation of a model. The resulting finite-model claim is a property of the logic; termination alone, for an arbitrary procedure, would not establish it.

Full first-order logic does not have the finite model property. For example, the first-order sentencerequires an irreflexive transitive relation with a successor for every element. It is satisfied by the usual strict order on the natural numbers. In a nonempty finite domain, repeatedly taking successors eventually repeats an element; transitivity would then force $R(x,x)$, contradicting irreflexivity. Hence this satisfiable first-order sentence has no finite model.

Use the substitution version of TBox unfolding from part (a), and abbreviateThe notation $\overline{L}$ is the negation normal form of $\neg L$. The unfolded input description logic concept isFor the remaining TBox, turn each general concept inclusion $X⊑Y$ into $\neg X\bigsqcup Y$, and unfold all defined names. The global description logic concept to add at every generated node isIn the last line, negating $\exists R.(\exists R.A\bigsqcup \exists R.B)$ gives $\forall R.(\forall R.\neg A\sqcap \forall R.\neg B)$. Both levels of universal restriction are needed.

Start the tableau algorithm for ALC with a root $x$ labelled $D^{\prime }$ and $\Gamma$. Expand the logical conjunctions. For the disjunction from (2), choose $\forall R.\overline{L}$. For the disjunction from (3), choose $\forall R.L$. Apart from the compound formulas already processed, the root label isThere is no existential restriction at $x$, so no successor needs to be generated. In particular, $\forall R.\exists P.\top$ creates a $P$-successor only at an existing $R$-successor; it creates no $R$-successor itself. The branch is complete and has no tableau clash. There is $\boxed{\text{no directly blocked node}}$: the open completion graph has only its root. The universal restrictions can have incompatible fillers without creating a tableau clash when there are no successors.

For comparison, choosing the other alternative $\exists R.\exists R.L$ from (2) creates an $R$-successor $y$. The root restriction $\forall R.(L\sqcap B)$ puts $A_0,\neg B,B$ in $\mathcal{L}(y)$, giving a tableau clash immediately. That branch closes before direct blocking in description logic is needed. The figure records the processed formulas through the label $\Gamma$ and displays the decisive labels explicitly.

A concrete model confirms the open branch:All three remaining general concept inclusions hold because their relevant $R$-successor requirements are vacuous. The definition of $C$ and the disjointness condition hold as well. Thus $\boxed{D\text{ is satisfiable with respect to }\mathcal{T}}$.

Using the absorbed TBox with its primitive inclusion, translate description logic concepts as unary predicates and description logic roles as binary predicates. Concept satisfiability means that some element belongs to $A\sqcap C$, while every element satisfies the TBox axioms. The required first-order sentence isOnly ${\mathcal{T}}_u$ is included here, as requested. There is no requirement to satisfy (1), (2) or (3). For instance, one element with $A=C=\{d\}$, $B=\varnothing$ and $P=\{(d,d)\}$ satisfies this first-order sentence.

Alternatively, unfolding the absorbed TBox first gives the existential first-order sentence $\exists x\exists y(A_0(x)\wedge \neg B(x)\wedge P(x,y))$. The interpretation of the eliminated names is then recovered by $A=A_0\setminus B$ and $C=\{x:\exists yP(x,y)\}$.

For EL with bottom, the eligible axioms are $\boxed{(2),(4),(5)}$. Axioms (1) and (3) contain universal restrictions, and (3) also contains a disjunction, so they are outside its syntax. For plain EL, whose constructors are $\top$, atomic names, conjunction and existential restriction, the eligible axioms are $\boxed{(2),(5)}$; (4) is excluded because it uses $\perp$. These conventions should not be conflated.

Here is a normalized TBox for the bottom-inclusive version. Introduce one fresh description logic concept $X$ for $\exists R.A$, and useThese are the usual normalized forms: an existential restriction on the left with an atomic right-hand side, an atomic left-hand side with an existential restriction on the right, or a conjunction of atomic names implying $\perp$. Here $\top$ is permitted as a filler.

The first two general concept inclusions force $X\equiv \exists R.A$. The third then says $\exists R.A⊑\exists R.\exists R.A$, exactly (2). Conversely, any model of (2) extends by $X=(\exists R.A{)}^{\mathcal{I}}$ to satisfy all three normalized general concept inclusions. The last two are the two directions of (5). For plain EL, delete just $A\sqcap B⊑\perp$ from this normalized TBox.

The standard semantics of ALC and EL do not impose the unique name assumption. Therefore the two individual names may denote the same element. A minimum-size model of either normalized TBox from part (d), together with the ABox, isThe $R$ self-loop supplies the ABox fact and makes both $\exists R.A$ and $\exists R.X$ true at $d$. The $P$ self-loop supplies exactly the existential restriction defining $C$. Disjointness holds because $B$ is empty. Hence every normalized general concept inclusion is satisfied. A domain must be nonempty, so $\boxed{|{\Delta }^{\mathcal{I}}|=1}$ is minimal.

If a separate unique name assumption were imposed, the minimum would instead be two. One can take $a\ne b$, $A=\{a\}$, $C=\{b\}$, $R=\{(a,b)\}$, $P=\{(b,b)\}$ and $B=X=\varnothing$. There is then no $R$-edge ending at an $A$ element, so the normalized requirements involving $X$ hold vacuously. That additional convention is not part of standard description logic semantics.

For plain EL, $\boxed{\text{every concept is satisfiable with respect to every EL TBox}}$. On a one-element domain, interpret every atomic description logic concept as the whole domain and every description logic role as the full binary relation. A structural induction makes every EL description logic concept denote that element. Every general concept inclusion is consequently true, including cyclic ones. The decision procedure can therefore always answer yes on well-formed inputs.

For EL with bottom, concept satisfiability with respect to general TBoxes is $\boxed{\text{P-complete}}$ under the usual logarithmic-space reductions. Polynomial-time completion propagates atomic inclusions, conjunction consequences and existential requirements; deriving $\perp$ for the queried description logic concept detects unsatisfiability. There are polynomially many such labels and normalized relationships to propagate.

For the lower bound, encode a monotone Boolean circuit with a starting description logic concept $S$. Give each input gate labelled one an inclusion $S⊑G_i$. Encode an AND gate by $G_i\sqcap G_j⊑G_k$, and an OR gate by $G_i⊑G_k$ and $G_j⊑G_k$. Finally add $G_{\mathrm{out}}⊑\perp$. Then $S$ is unsatisfiable exactly when the circuit output is one. The complement version is also P-complete, since P is closed under complement. Thus allowing $\perp$ changes a trivial satisfiability problem into a nontrivial polynomial-time one. The bottom-inclusive convention is also reflected in the ^[ref].

The satisfiability problem is $\boxed{\text{decidable}}$. Partition the positive facts according to their predicate symbols. Let ${\mathcal{A}}_{\mathcal{T}}$ contain those using description logic concepts or description logic roles from $\mathcal{T}$. Run an ordinary ALC knowledge base consistency procedure on $(\mathcal{T},{\mathcal{A}}_{\mathcal{T}})$. Return no if it is inconsistent, and yes otherwise.

The no answer is sound because any model of the whole knowledge base would restrict to a model of $(\mathcal{T},{\mathcal{A}}_{\mathcal{T}})$. For the converse, take a model $\mathcal{I}$ of that ALC part. Keep its domain, individual interpretations and TBox predicates. Interpret every predicate used by the positive Datalog rules as the full relation of its arity on this same domain. This is possible because those predicates are disjoint from the TBox predicates. Every Datalog rule head is then true under every variable assignment, so every positive rule and every remaining positive fact is satisfied. Predicates occurring only in facts can likewise be interpreted as full relations. Any individual name not already interpreted can denote an arbitrary domain element.

Consequently,The argument depends on both restrictions in the question: disjoint predicate vocabularies and positive rule heads. A rule concluding $\perp$ would not be made true by filling all relations. Sharing constants alone causes no problem, since the expansion uses the same domain and the same interpretations of those constants.

A concept satisfiability procedure that expands concept labels into a graph, branches on disjunctions, creates witnesses for existential restrictions, propagates universal restrictions along existing edges, and tests for a tableau clash. General TBoxes require global constraints and a termination device such as direct blocking in description logic.