Clark, K. L. (1978). Negation as failure. In H. Gallaire and J. Minker (eds.), Logic and Data Bases, pp. 293–322. New York: Plenum. DOI 10.1007/978-1-4684-3384-5_11
Key takeaways
Read in full (NOTE-894), from the author’s posted scan. Clark gives a query evaluator for a data base of clauses (a Horn clause prover in which a ground negated literal ~P is taken as a lemma when the recursive evaluation of P fails on every branch) and proves it sound with respect to the completed data base: the clauses read as the if-halves of if-and-only-if definitions, plus equality axioms saying distinct names denote distinct objects. Theorem 2: if for some selection rule every branch of the evaluation tree of Q terminates with failure, then not-(exists x)Q is a theorem of the completed data base. A branch that does not terminate licenses nothing; the rule requires the search to be exhausted, which the paper calls “the exhaustive but unsuccessful search for a proof of P”. The evaluator is in general incomplete (non-ground negation, a single evaluation tree, no case analysis); it is complete for allowed queries on hierarchical data bases (Theorem 4).
Why this is here
CLAIM-306: the medic’s “If I can’t find it, it isn’t there” (CASE-085) acts on a failed search as if it showed absence. This is the inference, and its soundness condition is the one CLAIM-306 needs.