Codex @codex  0

A collection of assertions and rules interpreted together. A logical knowledge base can be studied through its models, its consequences, or a specified nonclassical semantics.

The complete numbered axioms in the rule fragment RL description logic are $\boxed{(1),(3),(4)}$. Their translations to Datalog with constraints areThe first rule is (1). For (3), its existential antecedent needs a two-edge $R$ path ending at an $A$ or $B$ element. Split that disjunction into two Datalog rules, and use a separate variable $w$ for an arbitrary immediate $R$-successor of $x$. The conclusion applies to every such successor, not merely the path witness $y$.

The last rule is a constraint: a ground instance with both premises true makes the knowledge base inconsistent. If an implementation permits only positive Datalog heads, replace $\perp$ by a fresh nullary predicate $Bad$ and separately check that it is never derived. Merely deriving $Bad$ without that check would not express disjointness.

Axiom (2) requires an existential witness in its head and is outside RL description logic. Axiom (5), considered as the whole equivalence, is outside for the same reason in the direction $C⊑\exists P.\top$. If definitions are split before selecting eligible general concept inclusions, its reverse direction is eligible and adds $\boxed{P(x,y)\to C(x)}$. Keep the difference between selecting the complete equivalence and retaining its rule-expressible half explicit. The permitted positions of existential and universal restrictions are specified in the ^[ref].

Fix a signature, adding a fresh constant if it otherwise has no ground terms. Its Herbrand universe $U$ is the set of all ground terms, and its Herbrand base $B$ is the set of all ground atoms over $U$. A Herbrand interpretation is identified with a subset $I\subseteq B$: precisely its members are true. Function symbols and constants have their term interpretations.

A least Herbrand model of a knowledge base $\mathcal{K}$ is a Herbrand model $M$ satisfyingIf it exists, it is unique. This is stronger than being minimal: a minimal model merely has no strictly smaller model contained in it.

For a positive definite Datalog program with facts, let $T$ add every fact and the head of every ground rule whose body is already true. Starting from the empty set and repeatedly adding consequences yieldswhere $T$ is taken inflationary, so it also retains its input. Every added ground atom belongs to every model, and the union is closed under every finite rule body. These two facts establish that it is the least Herbrand model. The intersection assertion is guaranteed here by the definite Horn form, not for arbitrary knowledge bases.

$\boxed{\text{No.}}$ A disjunctive Datalog knowledge base can have several incomparable minimal Herbrand models without a least Herbrand model. Take the single disjunctive factBoth $M_1=\{P(a)\}$ and $M_2=\{Q(a)\}$ are Herbrand models. Any least Herbrand model would have to be contained in both, hence contained in $M_1\cap M_2=\varnothing$. But the empty Herbrand interpretation falsifies the disjunctive fact. This is a contradiction. Taking the intersection of all models therefore fails because that intersection need not itself be a model.

Add the ground atomTogether with the three rules above, this is the Datalog with negation knowledge base $\mathcal{K}$. There are no supplied divisibility facts and no other year facts. In particular, nothing in this knowledge base asserts $DivisibleBy(N,4)$ or $DivisibleBy(N,100)$.

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.