Signed data dependencies in logic programs

AbstractLogic programming with negation has been given a declarative semantics by Clark's completed database (CDB), and one can consider the consequences of the CDB in either two-valued or three-valued logic. Logic programming also has a proof theory given by SLDNF derivations. Assuming the data-dependency condition of strictness, we prove that the two-valued and three-valued semantics are equivalent. Assuming allowedness (a condition on occurrences of variables), we prove that SLDNF is complete for the three-valued semantics. Putting these two results together, we have completeness of SLDNF deductions for strict and allowed databases and queries under the standard two-valued semantics. This improves a theorem of Cavedon and Lloyd, who obtained the same result under the additional assumption of stratifiability