A quantifier-free completion of logic programs
We present a proof theoretic approach to the problem of negation in logic programming. We introduce a quantifier-free sequent calculus which is sound for Negation as Failure. Some extensions of the calculus have 3-valued or intuitionistic interpretations.
KeywordsLogic Program Logic Programming Truth Table Atomic Formula Proof Theory
Unable to display preview. Download preview PDF.
- A. Avron. Foundations and proof theory of 3-valued logics. LFCS Report 88-48, University of Edinburgh, Apr. 1988.Google Scholar
- L. Cavedon and J. W. Lloyd. A completeness theorem for sldnf-resolution. Technical Report 87/9, University of Melbourne, 1987.Google Scholar
- S. Cerrito. Negation as failure — a linear axiomatization. Technical Report 434, Université Paris X, 1988.Google Scholar
- K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases. Plenum Press, New York, 1978.Google Scholar
- J.-Y. Girard. Proof Theory and Logical Complexitiy. Bibliopolis, Napoli, 1987.Google Scholar
- H. Hodes. Three-valued logics: An introduction, a comparison of various logical lexica, and some philosophical remarks. Annals of Pure and Applied Logic, 2(43):99–145, 1989.Google Scholar
- G. Jäger. Proofs as advanced and powerful tools. In Proceedings of the XI IFIP Congress, 1989.Google Scholar
- K. Kunen. Signed data dependencies in logic programs. Technical Report 719, University of Wisconsin-Madison, Oct. 1987.Google Scholar
- J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, second edition, 1987.Google Scholar
- K. Schütte. Vollständige Systeme modaler und intuitionistischer Logik. Springer-Verlag, 1968.Google Scholar
- J. C. Shepherdson. Negation in logic programming. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming. Morgan Kaufmann, Los Altos, 1987.Google Scholar
- G. Takeuti. Proof Theory. North-Holland, Amsterdam, 1987.Google Scholar