A quantifier-free completion of logic programs

  • Robert F. Stärk
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 440)


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.


Logic Program Logic Programming Truth Table Atomic Formula Proof Theory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A. Avron. Foundations and proof theory of 3-valued logics. LFCS Report 88-48, University of Edinburgh, Apr. 1988.Google Scholar
  2. [2]
    L. Cavedon and J. W. Lloyd. A completeness theorem for sldnf-resolution. Technical Report 87/9, University of Melbourne, 1987.Google Scholar
  3. [3]
    S. Cerrito. Negation as failure — a linear axiomatization. Technical Report 434, Université Paris X, 1988.Google Scholar
  4. [4]
    K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases. Plenum Press, New York, 1978.Google Scholar
  5. [5]
    J.-Y. Girard. Proof Theory and Logical Complexitiy. Bibliopolis, Napoli, 1987.Google Scholar
  6. [6]
    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
  7. [7]
    G. Jäger. Proofs as advanced and powerful tools. In Proceedings of the XI IFIP Congress, 1989.Google Scholar
  8. [8]
    K. Kunen. Negation in logic programming. Journal of Logic Programming, 4(4):289–308, 1987.CrossRefGoogle Scholar
  9. [9]
    K. Kunen. Signed data dependencies in logic programs. Technical Report 719, University of Wisconsin-Madison, Oct. 1987.Google Scholar
  10. [10]
    J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, second edition, 1987.Google Scholar
  11. [11]
    K. Schütte. Vollständige Systeme modaler und intuitionistischer Logik. Springer-Verlag, 1968.Google Scholar
  12. [12]
    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
  13. [13]
    J. C. Shepherdson. A sound and complete semantics for a version of negation as failure. Theoretical Computer Science, 65(3):343–371, 1989.CrossRefGoogle Scholar
  14. [14]
    G. Takeuti. Proof Theory. North-Holland, Amsterdam, 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Robert F. Stärk
    • 1
  1. 1.Institut für Informatik und angewandte MathematikUniversität BernBern

Personalised recommendations