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 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 a satisfiable equality-free universal logical conjunction of Horn clauses, intersecting the sets of true ground atoms of its Herbrand models gives another Herbrand model, contained in every one of them. A ground atom is true in this least Herbrand model exactly when it holds in every Herbrand model. Positive existential sentences are true in the least Herbrand model exactly when they follow from the Horn clauses; allowing negated atoms makes this equivalence fail. For example, the least Herbrand model of $\forall x(P(x)\to Q(x))$ over a single constant $a$ makes both predicates empty and satisfies $\exists x\neg P(x)$, whereas the first-order structure making both predicates universal is a countermodel to that consequence.

The four-page University of Oxford Finals computer science examination held on 10 June 2015, Trinity Term 2015. Public primary-source archive: Lawrence Attachment.zip, member 2015-landp.pdf. Printed p. 4, Question 3(d), permits an arbitrary quantifier-free formula in an asserted least Herbrand model equivalence; that assertion fails when negative atoms are allowed, even for a satisfiable Horn clause.

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.

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.

A Herbrand interpretation $I$ is a stable model when it is the least Herbrand model of its stable model reduct ${\mathcal{K}}^I$. To form the reduct, ground the rules, delete each rule with a premise $\mathrm{not}A$ for which $A\in I$, and remove the remaining occurrences of not and their atoms.

For ${\mathcal{I}}_1$, the rules concerning $N$ in the reduct aretogether with $Year(N)$. No rule has a divisibility atom in its head, so forward chaining produces no divisibility facts and no leap fact. Ground rules for the other constants cannot fire because their year premises are absent. ThusTherefore $\boxed{{\mathcal{I}}_1\text{ is stable}}$.

For ${\mathcal{I}}_2$, the rule using $\mathrm{not}DivisibleBy(N,100)$ is deleted. The common-year rule is retained without its negative premise, since $Leap(N)$ is absent. Crucially, the reduct does not convert atoms already in ${\mathcal{I}}_2$ into facts. Its least Herbrand model is again $\{Year(N),Common(N)\}$. The two divisibility atoms in ${\mathcal{I}}_2$ have no support. Hence

Inspecting these two interpretations alone is not sufficient for skeptical entailment. That requires every stable model to contain $Common(N)$. Here we can finish the argument: every reduct has no rule deriving divisibility atoms, so every stable model has empty divisibility relation. Its leap relation must then be empty as well. The common-year rule consequently derives $Common(N)$, and the only year fact is $Year(N)$. Thus ${\mathcal{I}}_1$ is the unique stable model, andThis final uniqueness argument, rather than the examination of just two candidate interpretations, establishes the required universal claim.

A safe one-rule Datalog with negation example with no stable model isThere are no variables, so no safety condition is violated. If $P(a)$ is absent from a proposed stable model, its reduct contains the fact $P(a)$, whose least Herbrand model contains $P(a)$. If $P(a)$ is present, the rule is deleted, and the reduct has empty least Herbrand model. Either choice disagrees with its reduct's least Herbrand model. Additional unsupported atoms cannot repair the disagreement. Hence there is no stable model.

Solutions to the three questions of the University of Oxford computer science Finals examination held on 10 June 2015. Question 3(d) has a false assertion as printed; its solution gives a countermodel and explains the additional hypotheses under which the usual least Herbrand model argument works.^[ref]

The assertion is false as printed, even for a satisfiable equality-free Horn clause. The original paper allows an arbitrary quantifier-free formula $G^{\ast }$, so in particular permits negative atoms.^[ref]

Take a first-order signature with a constant $a$ and unary predicates $P,Q$, and letThe matrix of $F$ is a Horn clause, and the Herbrand universe is the singleton $\{a\}$. The possible Herbrand models of $F$ assign $(P(a),Q(a))$ the values $(0,0)$, $(0,1)$, or $(1,1)$. Neither ground atom is true in every such Herbrand model, so the paper's intersection construction givesConsequently ${\mathcal{H}}_F\models G$, with witness $a$. However, the one-element first-order structure in which both predicates hold everywhere satisfies $F$ and falsifies $G$. HenceThis directly refutes the requested implication; no proof of the stated equivalence is possible. It also isolates the issue: an atom being absent from the intersection means that it is false in some Herbrand model, not that it is false in every first-order model.

The standard correct version assumes that $F$ is satisfiable, uses an equality-free first-order signature with a nonempty Herbrand universe, and requires $G^{\ast }$ to be a positive quantifier-free formula: one built from atoms and truth constants using only logical conjunction and logical disjunction. Under those assumptions the expected argument is as follows.

First, the intersection of the ground atoms true in all Herbrand models is itself a Herbrand model of $F$. To see this, read each ground Horn clause as $A_1\wedge \cdots \wedge A_k\to B$, where $B$ is an atom or false. If every $A_i$ is true in the intersection, every $A_i$ is true in every Herbrand model. When $B$ is an atom, all these Herbrand models must make $B$ true, so the intersection does too. When $B$ is false, the antecedent cannot hold in any Herbrand model; since there is at least one such model, it cannot hold in the intersection either. Thus the intersection is the least Herbrand model.

Now let ${\mathcal{H}}_F\models G$ for positive $G^{\ast }$. There is a tuple of ground terms $\bar{t}$ with ${\mathcal{H}}_F\models G^{\ast }(\bar{t})$. Expand the positive quantifier-free formula into disjunctive normal form; one of its logical conjunctions of positive atoms is true at $\bar{t}$. Each of those ground atoms $A$ holds in every Herbrand model of $F$. It also follows that $F\models A$: otherwise a first-order model of $F\wedge \neg A$ would, by Herbrand's theorem for universal equality-free first-order clauses, yield a Herbrand model of $F\wedge \neg A$, a contradiction. Every first-order model of $F$ therefore satisfies the same positive logical conjunction at the interpretations of $\bar{t}$, and hence satisfies $G$.

Conversely, if $F\models G$, the fact that the least Herbrand model is a first-order model of $F$ immediately gives ${\mathcal{H}}_F\models G$. Thus the repaired conclusion isThe satisfiability qualification is separately necessary when general Horn clauses may have no positive conclusion. For instance, $F=\forall x(P(x)\wedge \neg P(x))$ is a logical conjunction of Horn clauses with no models. The intersection convention then makes every ground atom true by vacuity, yet $F$ entails even $\exists x\neg P(x)$, which that Herbrand structure falsifies. The earlier satisfiable example already refutes the printed claim without relying on this further defect.

A Herbrand interpretation equal to the least Herbrand model of the positive reduct obtained relative to that interpretation.

Ground the rules, delete every rule having a negative body atom true in the candidate $I$, and remove all remaining negative premises. The result is a positive program whose least Herbrand model is compared with $I$.

A semantics in which an interpretation must equal the least Herbrand model of its own stable model reduct. Some programs have no stable model, and others have several.