A linear axiomatization of negation as failure. (English) Zbl 0754.68025

Cerrito, Serenella

J. Log. Program. 12, No. 1-2, 1-24 (1992).

Summary: This paper is concerned with the axiomatization of success and failure in propositional logic programming. It deals with the actual implementation of SLDNF in PROLOG, as opposed to the general nondeterministic SLDNF evaluation method. Given any propositional program \(P\), a linear theory \(\mathbf{LT}_ P\) is defined (the linear translation of \(P\)) and the following results are proved for any literal \(A\):
soundness of PROLOG evaluation (if the goal \(A\) PROLOG-succeeds on \(P\), then \(\mathbf{LT}_ P\vdash_{\text{lin}}A\), and if \(A\) PROLOG-fails on \(P\), then \(\mathbf{LT}_ P\vdash_{\text{lin}}A^ \perp\)), and
completeness of PROLOG evaluation (if \(\mathbf{LT}_ P\vdash_{\text{lin}}A\), then the goal \(A\) PROLOG-succeeds on \(P\), and if \(\mathbf{LT}_ P\vdash_{\text{lin}}A^ \perp\), then \(A\) PROLOG-fails on \(P\)).
Here \(\vdash_{\text{lin}}\) means provability in linear logic, and \(A^ \perp\) is the linear negation of \(A\).

MSC:

68N17

Logic programming

Keywords:

SLDNF; PROLOG; soundness; completeness