Fix a signature, adding a fresh constant if it otherwise has no ground terms. Its Herbrand universe is the set of all ground terms, and its Herbrand base is the set of all ground atoms over . A Herbrand interpretation is identified with a subset : precisely its members are true. Function symbols and constants have their term interpretations.
A least Herbrand model of a knowledge base is a Herbrand model 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 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 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.
A disjunctive Datalog knowledge base can have several incomparable minimal Herbrand models without a least Herbrand model. Take the single disjunctive factBoth and are Herbrand models. Any least Herbrand model would have to be contained in both, hence contained in . 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.
Use
not for negation as failure, rather than classical logical negation. The disjunctive condition is expressed by two separate Datalog with negation rules:The positive premise restricts the rule to years and makes the variable explicitly safe. The divisibility relation is input data; the integer-looking constants do not make arbitrary arithmetic facts true automatically.The remaining classification rule isThe positive premise restricts the rule to years. Its negation as failure premise is evaluated by stable model semantics; it does not assert a separately stored negative fact. This gives a stratified Datalog program: divisibility and year facts are inputs, leap status is computed next, and common status last.
Add the ground atomTogether with the three rules above, this is the Datalog with negation knowledge base . There are no supplied divisibility facts and no other year facts. In particular, nothing in this knowledge base asserts or .
A Herbrand interpretation is a stable model when it is the least Herbrand model of its stable model reduct . To form the reduct, ground the rules, delete each rule with a premise for which , and remove the remaining occurrences of
not and their atoms.For , the rules concerning in the reduct aretogether with . 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 .
For , the rule using is deleted. The common-year rule is retained without its negative premise, since is absent. Crucially, the reduct does not convert atoms already in into facts. Its least Herbrand model is again . The two divisibility atoms in have no support. Hence
Inspecting these two interpretations alone is not sufficient for skeptical entailment. That requires every stable model to contain . 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 , and the only year fact is . Thus 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 is absent from a proposed stable model, its reduct contains the fact , whose least Herbrand model contains . If 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.
For polynomial-time many-one reductions, an unconditional example is the empty language:A procedure that rejects every input decides it in constant time, so it belongs to P and hence NP. It is not NP-hard: the nonempty formal language belongs to NP, but no many-one reduction can satisfyThe right-hand side is always false. Thus the hardness condition fails without assuming . Giving an ordinary nontrivial problem in P would not establish the requested separation unconditionally, because that would require excluding the possibility .
The halting problem is an unconditional example:Reduce SAT to it as follows. Given a Boolean formula , construct a Turing machine that ignores its input, enumerates all Boolean valuations of , and halts if it finds a satisfying one. If none satisfies , it enters an infinite loop after the enumeration. ThenThe construction of the machine description takes polynomial time; the potentially exponential running time of the constructed machine is irrelevant to the time needed to compute the polynomial-time reduction. Since SAT is NP-complete, this proves NP-hardness of the halting problem.
Every problem in NP is decidable, by enumerating the finitely many polynomial-length certificates and running the verifier. The halting problem is undecidable, so it is outside NP and therefore cannot be NP-complete.
The satisfiability problem is . Partition the positive facts according to their predicate symbols. Let contain those using description logic concepts or description logic roles from . Run an ordinary ALC knowledge base consistency procedure on . 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 . For the converse, take a model 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 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.
Articles by others on the same topic
There are currently no matching articles.