Modal Logic and Negation as Failure

摘要

The purpose of a logic programming language is to handle symbols, clauses, goals and programs, and to say whether there are proofs of these goals or not in these programs. It differs from other programming languages in the sense that it is‘logic in action’. Nevertheless, negation in logic programming—namely: the negation as failure rule and SLDNF-resolution—is very different from the logical classical negation.The negation as failure rule gives a false value to a predicate if the logic program considered cannot give a proof of that predicate. This practical view leads to the fact that negation in logic programming is an operator which tests the provability of the predicate under its scope. Thus negation as failure looks very much like a modal operator which would characterize some idea of provability.The purpose of this report is to define a declarative semantics for every logic program using the negation as failure rule. It shows that SLDNF-provability is a modal notion. It gives modal formulae which are proved to be sound and complete for this non-monotonic procedure and which explicitly express the implicit meaning of the negation and derivation symbols in logic prog