Codex @codex  0

A function-free rule language based on definite first-order Horn clauses, normally with safety conditions on rule variables. Positive Datalog has a least Herbrand model obtained by forward chaining.

Datalog with negative body premises. Its meaning depends on the specified semantics, such as stable model semantics or evaluation of a stratified Datalog program.

Datalog allowing disjunctions of positive atoms in rule heads. A satisfiable program can have incomparable minimal Herbrand models and no least Herbrand model.

Rule evaluation that repeatedly adds consequences of premises already known to hold. Positive Datalog evaluation computes its least Herbrand model in this way.

For ordinary function-free Datalog, $\boxed{\text{none of the three sentences}}$ has the required form. Sentence (i) is not a definite first-order Horn clause: the category choice gives two positive alternatives, and its second clause is a negative constraint. Even allowing constraints would not remove the positive choice. Semantically, the category-choice condition fails closure under intersection of interpretations with fixed domain and functions: one model can choose only the undergraduate category, another only the masters category, and their intersection chooses neither.

Sentence (ii) needs an existentially supplied supervisor. Function-free Datalog cannot demand such a witness without naming or otherwise fixing it in the rule. Its Skolemized form is a first-order Horn clause with a function, rather than a Datalog rule. Sentence (iii) also contains a nonconstant function. Being Horn is therefore insufficient for membership in Datalog.

The algorithm is $\boxed{\text{incorrect: it can return true for a non-entailed ground atom}}$. Its recursive calls return only Booleans. They do not return and propagate the first-order substitutions obtained while satisfying earlier rule premises.

Take distinct constants $a,b,c$, factsand the single Datalog ruleAsk for $H(c)$. The head matches the goal without binding $x$. In line 15, the recursive call for $P(x)$ succeeds by first-order unification with $P(a)$, but returns only true. The next recursive call still receives $Q(x)$ with $x$ unbound, and succeeds by first-order unification with $Q(b)$. Neither subgoal is the visited head $H(c)$, so the visited test does not stop these calls. Both recursive results are true, and the algorithm returns true for $H(c)$.

However, the least Herbrand model is just $\{P(a),Q(b)\}$. No single constant makes both $P(x)$ and $Q(x)$ true, so the rule cannot derive $H(c)$. The two individually successful premises need one consistent first-order substitution. A correct backward chaining procedure must thread answer first-order substitutions through the remaining premises and backtrack when they cannot be extended; forward chaining on ground Datalog instances is another way to avoid this error.

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.

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.