TLDR
- Absence becomes negative only after search. To infer not P, every proof path for P must finitely fail.
- Operational failure needs declarative meaning. Clark interprets database clauses as completed if-and-only-if definitions.
- Names need a free equality theory. Distinct constants and constructors must behave as distinct data objects.
- Soundness is not completeness. Successful and finite failed evaluations are licensed by completion, yet some consequences remain undiscoverable.
- Termination carries epistemic weight. A loop is neither success nor failure, so it cannot support a negative conclusion.
Positive clauses do not answer negative questions by themselves
A logic database records facts and rules for what is true. Ordinary questions soon ask what is false. Clark’s problem is to make that step computationally efficient without pretending that silence is automatically a proof.
A conventional relation can list its members. A logic database also contains intensional clauses: general rules from which unlisted instances may be derived. If Takes(Ada, C101) is absent, it might still follow from a rule. Looking only for a stored tuple is therefore insufficient.
Prolog and Planner used a pragmatic rule. To evaluate a ground negative literal not P, launch a proof search for P. If a proof succeeds, not P fails. If every possible proof path finitely fails, accept not P. Clark names and analyses this negation-as-failure rule.
The word “every” is load-bearing. Failure of one attempted clause says only that one route did not work. Exhaustive failure closes all available routes. Nontermination leaves a route open indefinitely. Negation as failure is consequently a property of a completed search tree, not of the first disappointing branch.
This rule assumes a kind of informational closure. If the database provides all ways a relation may hold, and none applies, the instance is false. Reiter’s closed-world assumption expresses a related intuition. Clark makes the closure explicit by transforming clauses into predicate definitions and adding axioms for the data constructors.
The paper’s achievement is double. It gives operational rules that map naturally onto backtracking implementation, and it proves that certain outcomes are consequences of the completed database. It also refuses a triumphalist ending: query evaluation is incomplete in general, sensitive to termination and literal selection, and complete only under strong restrictions.
Worked example 1 · an unlisted course
The database contains only Maths-course(C101) and Maths-course(C301), with no general rule. Search for Maths-course(C201) tries both facts and both unifications fail. Under the completed definition and distinct-name axioms, not Maths-course(C201) follows.
Causal probe 1 · add a new course tomorrow
The earlier negative answer can disappear. Negation as failure is nonmonotonic with respect to database extension: adding a fact or rule opens a proof that a formerly exhaustive failure had closed. The inference described the completed database then, not an eternal world.
A logic database is both stored data and a programme of deductions
Clark writes every database clause with one distinguished positive literal. Its remaining literals form the conditions under which that head relation holds.
A clause has the form R(t₁,…,tₙ) ← L₁ ∧ … ∧ Lₘ. When m is zero it is a unit fact. Ground unit clauses provide explicit relation instances; non-unit clauses constitute the intensional component. Variables are implicitly universally quantified across the implication.
The paper’s micro-database names two students, records courses they take, lists two mathematics courses and defines a non-mathematics-major. The rule says that x is a non-mathematics-major if some mathematics course y exists that x does not take. Negation occurs in a rule body rather than as a stored negative fact.
A query is a conjunction of literals. Its free variables request constructive substitutions. The query Student(x) ∧ Takes(x,C101) asks for a witness x; a successful evaluation returns bindings. A ground query returns true if it succeeds. It returns false only when its entire evaluation tree fails.
More expressive quantified questions can be compiled into this standard form using auxiliary predicates. “Find students who take every mathematics course” becomes “find a student for whom there is no mathematics course not taken”. The auxiliary relation packages the existential counterexample.
This transformation reveals why negation is not a decorative operator. Universal requirements often become the absence of a counterexample. Efficient negative evaluation therefore expands the kinds of database question that a Horn-clause engine can answer.
Worked example 2 · all mathematics courses
D. Smith takes C101 and C301, the two completed mathematics courses. The auxiliary query for a mathematics course Smith does not take has no successful branch. Its failure supports not Non-maths-major(D.Smith), which is the compiled form of taking them all.
Causal probe 2 · leave the course relation open
Failure to find a missed course no longer establishes that Smith takes every course; an undisclosed course might exist. Completion supplies the boundary that makes the universal-looking answer defensible.
Resolution grows a tree of clause alternatives
The evaluator is a non-deterministic linear-resolution procedure. Literal selection follows a rule; clause choice creates alternative branches.
At each step a selection rule chooses one literal from the current conjunction. Prolog’s familiar policy chooses the leftmost literal. The chosen clause is not fixed in the abstract evaluator: every database clause about the selected predicate offers an alternative path.
For a positive literal R(t), choose a clause whose head is about R and attempt unification. If unification succeeds with a most general unifier θ, replace the selected literal by the clause body and apply θ to the derived query. If it fails, that path ends in failure. If no clause defines R, the single next step fails.
A path succeeds when it reaches the empty query. The composition of its unifiers, restricted to the original query variables, is an answer. A path can also continue forever. These three outcomes: success, finite failure and nontermination: must remain distinct.
Clause choice creates branching because one relation may have several sufficient conditions. Literal choice ordinarily changes control rather than adding branches to the same evaluation tree. That distinction later matters: one selection rule can generate an infinite tree where another exposes a finite failure proof.
A complete traversal of a finite tree can enumerate every successful binding. Implementation need not materialise the tree. Stack frames can record the current clause, bindings and remaining alternatives; backtracking restores the next branch. The declarative tree explains what the efficient stack computation means.
Worked example 3 · two students, one course
For Student(x) ∧ Takes(x,C101), the first student fact binds x to J. Brown and the takes fact succeeds. Backtracking later binds x to D. Smith and also succeeds. The two successful paths yield two answers.
Causal probe 3 · stop after the first clause mismatch
The evaluator would confuse branch failure with query failure. Another clause might unify and succeed. Exhaustiveness over clause alternatives is the operational foundation of every later negative inference.
A ground negative literal launches a subsidiary proof search
For not P, the evaluator asks P as a new query. The result reverses only when the subsidiary evaluation is decisively complete.
If the positive query P succeeds on any path, not P fails. If every path in the evaluation tree for P finitely fails, not P is accepted as a lemma and deleted from the parent query. If the search has an infinite branch, neither result is licensed.
Clark restricts selection of negative literals to ground instances. Attempting not R(x) before x is bound would ask the failure procedure to return a constructive complement, which ordinary Prolog negation does not do. A selection rule must delay such a literal until positive goals instantiate its variables.
Subsidiary failure proofs can nest. Proving not P may explore P, whose clauses contain not Q, which launches a proof for Q. The soundness argument therefore uses induction both over the structure of failure trees and over the number of nested failure proofs.
The operational asymmetry is deliberate. To prove P, find one successful branch. To prove not P by failure, close every branch. Clause alternatives are existential for success but universal for failure. Literal-selection alternatives are not searched in the basic procedure, which creates one source of incompleteness.
Timeout is not logical failure. Resource bounds can make an implementation report “unknown” or stop, but Clark’s theorem concerns a genuinely finite tree whose every leaf fails. Replacing this condition with “the server waited long enough” changes the inference rule.
if ∃ successful proof path for P → not P FAILS
if every proof path for P finitely fails → infer not P
if any path remains infinite or unexplored → UNDECIDED
Worked example 4 · a known enrolment
The query not Takes(D.Smith,C101) launches the positive query. A matching unit clause succeeds immediately, so the negative literal fails. The rule does not let absence reasoning override positive evidence.
Causal probe 4 · select not Takes(x,C101) before Student(x)
The negative call contains a variable and can flounder. Selecting Student(x) first produces ground candidates, after which each negative test has the form required by the rule. Literal order changes operational safety.
Many sufficient clauses become one necessary-and-sufficient definition
Clark gives failure a first-order interpretation by reading the displayed clauses as the if-halves of definitions whose missing only-if halves are supplied by completion.
First put each clause for predicate R into a common head R(x₁,…,xₙ). Equalities connect the common variables to the original head terms, and variables local to the clause body are existentially quantified. The result Eᵢ is the clause’s general form.
If R has k clauses, its completion is R(x) ↔ E₁ ∨ … ∨ Eₖ. The forward direction groups the original rules: each body suffices for R. The reverse direction is new: if R holds, at least one listed clause condition explains it. If R has no clauses, its definition is R(x) ↔ false.
For facts P(a), P(b) and the recursive rule P(f(y)) ← P(y), completion yields P(x) ↔ x=a ∨ x=b ∨ ∃y[x=f(y) ∧ P(y)]. This is not merely a closed finite table; rules remain inside the definition.
Completion is predicate-specific and syntactic. It does not assert that every proposition unmentioned anywhere is false by a separate global axiom. It transforms the actual rule heads and bodies into relation definitions, accompanied by an identity theory for terms.
This declarative theory is stronger than the original implications. That strength is intentional: it states that the programme lists every way the predicate may be true. Whether such closure matches the intended application is a modelling decision, not a theorem delivered by the syntax alone.
general form Eᵢ(x) = ∃yᵢ [x=tᵢ ∧ Bodyᵢ]
completion: ∀x [R(x) ↔ E₁(x) ∨ … ∨ Eₖ(x)]
no defining clauses: ∀x [R(x) ↔ false]
Worked example 5 · completing Takes
Three unit facts for Takes become a definition whose right side is a disjunction of three pairs of name equalities. To prove someone does not take a course, first-order reasoning can eliminate each disjunct when its equalities contradict the queried names.
Causal probe 5 · read each original arrow as “if and only if” separately
That would make alternative clauses compete incorrectly: P(a) ↔ true and P(b) ↔ true do not share a common variable pattern. Completion first generalises heads, then disjoins every explanation into one predicate definition.
Failed matches become logical inequalities only under constructor axioms
Search knows that C101 and C301 do not unify. A first-order proof needs axioms explaining why those symbols denote different objects.
The identity theory includes ordinary equality: reflexivity, symmetry, transitivity and substitution. It also makes constants and function symbols free data constructors. Distinct constants denote distinct objects. Distinct functors construct distinct objects. A functor is injective in its arguments.
No constructed term equals a constant, and a variable cannot equal a proper term containing itself. These are the logical counterparts of the occurs check and of structural term comparison. They prevent accidental models in which a and b denote the same object or x equals f(x).
Clark’s unification lemma says that, under this identity theory, successful unification corresponds to an equivalent conjunction of equations representing the most general unifier. Failed unification makes the head-equality conjunction equivalent to false.
This bridge powers Theorem 1. Operationally, the evaluator tries clause heads. Declaratively, the completed predicate is a disjunction of generalised clause bodies guarded by head equalities. Unification either supplies the substitution that selects a disjunct or proves that disjunct impossible.
The result depends on term semantics. In a domain where two names may co-refer, or where equality is not free-constructor equality, match failure need not prove inequality. Negation as failure must therefore be interpreted relative to the completed database and its identity assumptions.
Worked example 6 · distinct course names
Trying Maths-course(C201) against the fact Maths-course(C101) produces the impossible equality C201=C101. A distinct-constants axiom refutes it. Without that axiom, the two symbols could denote one object in a first-order model.
Causal probe 6 · permit x=f(x)
Cyclic substitutions can destroy the finite-tree interpretation of data terms and invalidate the occurs-check correspondence. Clark’s identity schemas exclude such self-containing equalities.
Resolution, failure, exhaustive answers and restricted completeness must not be conflated
Clark’s theorem sequence moves carefully from one resolution step to an entire finite evaluation and then to a strongly restricted completeness result.
Theorem 1 connects a positive resolution step to completion. A query Q containing positive R(t) is equivalent, in the completed database, to the disjunction of the general forms of all resolvents obtained from clauses about R. If none exists, Q is equivalent to false.
Theorem 2 validates negation as failure. If, for some literal-selection rule, every branch of the evaluation tree rooted at ←Q terminates in failure, then the completed database proves not ∃x Q, where x are Q’s free variables. A finite failure tree is therefore a proof object.
Theorem 3 treats a tree whose every branch ends in success or failure. Assuming the completed database is consistent, the query is equivalent to the disjunction of the general forms of all returned answers. Exhaustive finite search establishes that the answer set is exact, not merely that each answer is sound.
Theorem 4 arrives only after examining incompleteness. For databases satisfying Clark’s hierarchical constraint, evaluation is complete for allowed queries. Relations are arranged in finite levels; rule bodies refer only to lower levels; recursion and mutual recursion are excluded. Negative variables are range-restricted by positive literals.
The quantifiers matter. Theorem 2 says “for some selection rule” and assumes every branch fails. It does not say a particular Prolog run can recognise every logical falsehood. Theorem 4 supplies that broader operational assurance only for a narrow, terminating class.
| Result | Premise | Conclusion | Does not promise |
|---|---|---|---|
| Theorem 1 | All positive resolvents of one selected literal | Query equals their general-form disjunction | Termination of later evaluation |
| Theorem 2 | Every branch of one evaluation tree finitely fails | Negated existential follows from completion | That such a tree will always be found |
| Theorem 3 | Every branch succeeds or fails; completion consistent | Returned answers are exactly the query solutions | Finite trees for arbitrary programmes |
| Theorem 4 | Hierarchical database; allowed query | Evaluation is complete | Recursion or unrestricted negation |
Worked example 7 · exact answers from a finite tree
If a query tree has three successful leaves returning x=a, x=b and x=c, while every other leaf fails, Theorem 3 licenses the completed-database equivalence Q(x) ↔ x=a ∨ x=b ∨ x=c, modulo each answer’s general form.
Causal probe 7 · infer completeness from soundness
A procedure may return only true answers yet miss true answers through looping or an impoverished proof rule. Theorem 2 and the sound half of Theorem 3 do not erase that gap.
Groundness, selection, case analysis and recursion open different holes
Clark devotes substantial attention to failure modes. They are not footnotes to the method; they specify exactly where procedural failure stops tracking classical consequence.
First, a negative literal with free variables cannot be selected. The query not R(x,a) asks constructively for objects outside R, but ordinary negation as failure can only test ground candidates. Allowed queries require variables in negative literals to be grounded by positive literals.
Second, one literal-selection rule may loop where another produces a finite failure tree. Clark’s example uses P(x) ← Q(y) ∧ R(y), recursive Q(h(y)) ← Q(y), and a ground R(g(y)) fact. Leftmost selection keeps expanding Q; selecting R exposes failure. The basic evaluator searches clause alternatives, not alternative selection rules.
Third, classical case analysis can derive consequences unavailable to sequential query evaluation. Two rules for R contain P and not P respectively, with matching Q and T facts. Classical logic can resolve across P ∨ not P, yet evaluation insists on deciding P. If P loops, the desired R consequence remains unreachable.
Fourth, recursive definitions make finite extension and termination nontrivial. Completion may be perfectly expressible while Prolog-style evaluation diverges. The paper therefore distinguishes declarative consequence from what its efficient procedure can discover.
Clark proposes a sufficient route around these holes. A database with computable finite relation extensions terminates on allowed queries. His hierarchical constraint guarantees that property by stratifying relation definitions into levels and prohibiting recursion. He calls it very strong; its honesty is part of the result.
Worked example 8 · a range-restricted negative test
Student(x) ∧ not Takes(x,C301) is allowed when Student(x) is selected first. It enumerates finite student names, then makes a ground Takes test for each. The positive literal supplies the candidate range that negation itself cannot construct.
Causal probe 8 · equate looping with false
In Clark’s selection example, that shortcut would make truth depend on which literal happened to be chosen first. A different control order exposes finite failure. Preserving “undefined by this run” prevents an operational accident becoming a logical fact.
Completion became a landmark, not the final word on negation
Later logic programming preserved Clark’s questions while developing semantics that handle recursion, cycles and incomplete information differently.
Shepherdson compared completed databases with Reiter’s closed-world assumption and identified conditions under which their consequences align or diverge. Subsequent criticism and refinement emphasised that completion is a chosen theory of programme meaning, not a neutral reading of every rule set.
Stable-model semantics treats negative body literals through a reduct and supports answer-set programming. Well-founded semantics assigns a unique partial model, often leaving atoms undefined when negative recursion prevents a justified two-valued decision. These approaches respond directly to the loop and case-analysis difficulties visible in Clark’s paper.
Fages-style tightness results later identify programmes for which stable models coincide with models of completion. The relationship is therefore structural: completion can be exactly right for important classes without being the only semantics for all normal programmes.
Operational research developed tabling, constructive negation and termination analysis. Tabling can prevent redundant loops and compute well-founded answers; constructive negation can return constraints for non-ground negative goals. These methods extend the query behaviour that Clark deliberately restricted.
None of this diminishes the 1978 contribution. Clark supplied a precise bridge between proof search and declarative theory, exposed its dependencies, and separated soundness from completeness. The later field can be read as an extended investigation of the boundary he drew.
Worked example 9 · mutual default negation
The programme p ← not q; q ← not p has two stable models, one containing p and one q. A two-valued completion also has corresponding models, while well-founded semantics leaves both undefined. Different semantics answer a question that a single Prolog failure run cannot settle neutrally.
Causal probe 9 · retrofit stable models into Clark’s theorem
Theorem 2 is about first-order consequences of the completed database under its stated procedure. Later semantic agreement requires additional results and programme conditions. Historical continuity does not make the formalisms interchangeable.
Watch success, exhaustive failure and looping produce three different answers
This deterministic laboratory models the exact decision boundary for a ground negative literal. It is deliberately small enough that every clause alternative and terminal status is visible.
Absent course tries both completed mathematics facts. C201 matches neither; all alternatives are closed and not Maths(C201) is accepted. The completion formula agrees because C201 differs from C101 and C301.
Present enrolment finds the stored Takes fact. One success is sufficient to make the negative query fail. Other alternatives do not need to fail before that conclusion.
Recursive P continually transforms P(a) into P(f(a)), P(f(f(a))) and so on under the displayed rule. The depth control changes only how much of the open path is drawn. No finite cutoff is labelled failure, so not P(a) remains undecided.
The three exact tests verify that a claim of exhaustive failure has inspected every clause alternative, that negation is accepted only for an all-failed finite positive tree, and that the displayed result agrees with the supplied completion status. The numbers and programmes are explanatory instances, not an experimental result from Clark.
The laboratory makes an important asymmetry tangible. Success is witnessed by one path; failure is certified by the closure of all paths; a loop withholds both. Negation as failure is therefore closer to a proof-tree protocol than to a textual search for a missing fact.
Worked example 10 · changing the depth display
At depth three the loop shows P(f(f(a))); at depth seven it shows a longer term. Neither view finds a failed leaf. A resource bound changes observation, not the logical status, so the answer remains undecided at every displayed cutoff.
Causal probe 10 · label depth seven “failure”
The same programme would make not P(a) true at depth seven and perhaps false if a base fact appeared at depth eight. That is bounded negation with different semantics, not Clark’s exhaustive-failure rule.
Separate programme meaning, search control and resource policy
A modern reconstruction should make three layers independently testable: the completion theory, the abstract evaluation tree and the concrete engine that traverses it.
Parse clauses into explicit heads and signed body literals. Standardise variables apart, implement unification with an occurs check and retain proof substitutions. Generate every clause alternative for a selected positive literal before declaring its tree failed.
Construct completion mechanically. For each predicate, generalise clause heads with equalities, existentially quantify local variables and disjoin bodies under one biconditional. Emit free-equality axioms appropriate to the term language. Test the output with small finite model finders or a first-order prover.
Represent outcomes as success with bindings, finite failure, flounder, loop or resource-unknown. Do not collapse the last three. Record the selection rule and branch order so a result can be replayed. Compare leftmost evaluation with fair search and tabling on Clark’s looping examples.
Reproduce Theorems 1–3 on bounded finite programmes by enumerating ground interpretations and proof trees. For completeness experiments, generate allowed hierarchical databases and then add one forbidden feature at a time: recursion, mutual recursion, an unbound negative variable or case-analysis dependence.
Extensions can compare Clark completion, stable models and well-founded semantics on the same normal programmes. The research question should be explicit: agreement of models, discoverability of queries, termination, or constructive negative answers. These are related but non-identical properties.
| Audit item | Minimum evidence | Failure prevented |
|---|---|---|
| Clause coverage | All heads tried for every failed positive node | Branch failure is called query failure |
| Groundness | Trace when each negative variable becomes bound | Floundering is reported as falsity |
| Termination | Cycle/open-path status distinct from failed leaf | Timeout becomes a theorem |
| Completion | Common heads, existential locals, one disjunction | Separate rules are closed incorrectly |
| Equality | Distinctness, injectivity and occurs check | Match failure lacks logical support |
| Semantic comparison | Named theory and programme class | Completion, stable and well-founded readings blur |
Worked example 11 · one-feature ablation
Start with an allowed hierarchy whose query tree is finite. Add only the recursive rule Q(h(y)) ← Q(y). If leftmost evaluation now loops while fair tabling terminates, the experiment attributes the change to recursion plus control rather than to negation in general.
Causal probe 11 · report only Boolean answers
The evaluation’s scientific content disappears. “False” could mean exhaustive failure, a loop cut off by timeout, floundering or no model under a later semantics. Typed outcomes preserve the assumptions behind the answer.
What survived formal, historical and delivery challenge
Review one: scholarly fidelity and teaching. The reconstruction was checked against Clark’s complete author-hosted scan, including its query algorithm, micro-database, completion construction, identity schemas, unification lemma, Theorems 1–4, selection-rule counterexample, case-analysis counterexample and hierarchical restriction.
The chief teaching risk was paraphrasing “not proved” as “false”. Every section preserves the stronger premise: a ground positive subsidiary query must have a finite tree whose every path fails. A second risk was treating completion as mere fact closure. The page retains general rules, existential local variables and free-constructor equality.
Review two: evidence fairness, language and accessibility. Soundness and completeness are separated. Theorem 3’s consistency and finite-tree premises remain visible. The hierarchical completeness condition is called strong, recursion is not smuggled into its scope, and later stable or well-founded semantics are contextual rather than retroactive.
All ten figures carry titles, descriptions, captions and source scopes. Animation is redundant, stops under reduced-motion preference and does not encode an otherwise invisible distinction. Controls are labelled, state is written as text, and the laboratory exposes three exact checks. British spelling and historical terminology are retained without imitating OCR errors.
Review verdict
Pass 1: formal reconstruction: passed after restoring universal branch closure, groundness, free equality and each theorem’s exact premise. Pass 2: evidence and delivery: passed after separating timeout, loop, flounder, classical consequence and later semantic alternatives.
Twelve cards for durable recall
Control moves from repairing a plan to interpreting an unsuccessful proof
Paper 0090 used explicit flaws to guide stochastic plan repair. Paper 0091 asks what a proof engine may conclude when every attempted repair of a query branch fails.
Both papers make failure structured. In LPG an unsupported precondition generates neighbouring plans. In Clark’s evaluator a failed positive subtree can license a negative lemma. Neither treats failure as a terminal word without recording why alternatives closed.
The difference is epistemic authority. LPG’s evaluation is heuristic: a low-cost move need not lead to an optimal plan. Clark’s finite failure tree supports a theorem of the completed database. Operational traces become logical evidence only because completion and equality provide a declarative interpretation.
Canon 0092 continues with Robert Kowalski’s “Algorithm = Logic + Control”. Clark has already exposed that equation in practice: the completion provides logic, the literal-selection rule provides control, and their separation explains both efficient execution and incompleteness.
Ignorance becomes negation only inside a declared boundary
Negation as failure is sometimes summarised as “if you cannot prove it, assume it is false”. Clark’s paper is more disciplined and more interesting than that slogan.
The relevant inability is not personal or temporary. It is an exhaustive result relative to a specified programme, term theory and selection discipline. Completion declares that the programme contains every explanation for each relation. Free equality lets failed matches eliminate those explanations. A closed proof tree witnesses that none survives.
Once any part of that boundary opens, the conclusion changes. A new clause can retract the negative fact. An infinite branch prevents closure. A non-ground query asks for a complement the evaluator cannot construct. A classical case split may establish a consequence that sequential control never reaches.
The paper therefore turns computational modesty into logical clarity. It does not eliminate the gap between world and database. It states the assumptions under which database failure can count as knowledge. That is the lasting lesson for agency: negative action needs a justified search boundary, not merely an empty result list.
Worked example 12 · no alert is not no danger
A monitoring programme can infer “not flagged” when every completed rule for flagging finitely fails. It cannot infer “not dangerous” unless danger itself has been completely defined by those rules. Predicate completion applies to the modelled relation, not to every real-world interpretation attached to its label.
Causal probe 12 · hide the completion assumption
Users will read an operational miss as a world fact. Making completion explicit reveals the true claim: given these exhaustive rules and these data constructors, no proof exists. That transparency is essential when negative conclusions trigger action.
Primary source, companion scope and verification contract
This companion reconstructs Keith L. Clark’s “Negation as Failure”, published in Hervé Gallaire and Jack Minker’s Logic and Data Bases (Plenum Press, 1978), pages 293–322, DOI 10.1007/978-1-4684-3384-5_11. The primary text was checked from Clark’s author-hosted scan. It covers clause databases, query evaluation, ground negative testing, completion, identity theory, the four theorem sequence, incompleteness examples, hierarchical completeness and later semantic context. All figures are original.
Verification contract. Five orientation claims, ten accessible animated SVG figures, twelve worked examples, twelve causal probes, twelve memory cards, two reviews and three executable exact tests. British English, reduced-motion support, responsive layouts, source boundaries and explicit unknown outcomes are included.
Primary and contextual sources
- Clark, K. L. (1978). “Negation as Failure.” In H. Gallaire & J. Minker (eds.), Logic and Data Bases, 293–322. Plenum Press. DOI; author-hosted scan.
- Reiter, R. (1978). “On Closed World Data Bases.” In Logic and Data Bases, 55–76.
- Kowalski, R. (1979). “Algorithm = Logic + Control.” Communications of the ACM, 22(7), 424–436.
- Apt, K. R., & van Emden, M. H. (1982). “Contributions to the Theory of Logic Programming.” Journal of the ACM, 29, 841–862.
- Shepherdson, J. C. (1984). “Negation as Failure: A Comparison of Clark’s Completed Data Base and Reiter’s Closed World Assumption.” Journal of Logic Programming, 1, 51–79.
- Gelfond, M., & Lifschitz, V. (1988). “The Stable Model Semantics for Logic Programming.” International Logic Programming Conference and Symposium, 1070–1080.
- Van Gelder, A., Ross, K. A., & Schlipf, J. S. (1991). “The Well-Founded Semantics for General Logic Programs.” Journal of the ACM, 38, 620–650.
- Fages, F. (1994). “Consistency of Clark’s Completion and Existence of Stable Models.” Methods of Logic in Computer Science, 1, 51–60.
- Lifschitz, V., & Turner, H. (2003). “Tight Logic Programs.” ACM Transactions on Computational Logic, 4, 507–522.
- Drabent, W., & Miłkowska, M. (2005). “Proving Correctness and Completeness of Normal Programs—a Declarative Approach.” Theory and Practice of Logic Programming, 5, 669–711.