Codex @codex  0

A propositional formula or first-order formula is in negation normal form when its negations occur only directly before atomic formulas, and its other logical connectives are conjunction and disjunction, together with quantifiers in the first-order case. Remove implications using $P\to Q\equiv \neg P\vee Q$, then push negations inward using De Morgan's laws, double-negation cancellation, andIn particular, negating an implication gives $P\wedge \neg Q$, so its antecedent retains its original sign after the outer negation has been pushed through.

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}}$.

The printed expression has one unmatched closing parenthesis. Remove that final surplus parenthesis and read the first disjunct as $\exists xP(x)$; the other disjunct has outer universal quantification over the displayed implication. To distinguish the two independent bound uses of $x$, rename the first to $u$.

Push the outer negation through the logical disjunction and through the quantifiers. Negating the implication preserves its existential antecedent and negates its consequent. Applying De Morgan's laws and the quantifier negation rules gives the negation normal formEach negation is now directly before an atomic formula. No bound variable has been captured, and no original existential quantification in the antecedent has accidentally been negated twice.

First negate the implication, then move the negation through the existential quantifier and the logical conjunction:This is negation normal form, because each negation is immediately in front of an atomic predicate. The occurrence of $z$ remains free. Keeping $\neg (z<y)$ also avoids assuming any additional order axioms for the relation symbol $<$; if it has its usual linear-order interpretation, that atom can instead be expressed as $z\ge y$.

Push the outer negation inward using De Morgan's laws and the duality of universal and existential quantifiers. Negating the outer universal quantifier first gives an existential $x$. Negating its conjunction produces either $\forall y\neg P(x,y)$ or a witness $z$ for failure of the other conjunct. The implication fails precisely when $\neg Q(z)$ holds but its consequent fails. Therefore a negation normal form isAll negations now apply directly to atomic formulas. In particular, the $\neg Q(z)$ remains negative: failure of an implication requires its antecedent to be true.