Abstract
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.
Preview
Unable to display preview. Download preview PDF.
References
A. Avron. Foundations and proof theory of 3-valued logics. LFCS Report 88-48, University of Edinburgh, Apr. 1988.
L. Cavedon and J. W. Lloyd. A completeness theorem for sldnf-resolution. Technical Report 87/9, University of Melbourne, 1987.
S. Cerrito. Negation as failure — a linear axiomatization. Technical Report 434, Université Paris X, 1988.
K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases. Plenum Press, New York, 1978.
J.-Y. Girard. Proof Theory and Logical Complexitiy. Bibliopolis, Napoli, 1987.
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.
G. Jäger. Proofs as advanced and powerful tools. In Proceedings of the XI IFIP Congress, 1989.
K. Kunen. Negation in logic programming. Journal of Logic Programming, 4(4):289–308, 1987.
K. Kunen. Signed data dependencies in logic programs. Technical Report 719, University of Wisconsin-Madison, Oct. 1987.
J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, second edition, 1987.
K. Schütte. Vollständige Systeme modaler und intuitionistischer Logik. Springer-Verlag, 1968.
J. C. Shepherdson. Negation in logic programming. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming. Morgan Kaufmann, Los Altos, 1987.
J. C. Shepherdson. A sound and complete semantics for a version of negation as failure. Theoretical Computer Science, 65(3):343–371, 1989.
G. Takeuti. Proof Theory. North-Holland, Amsterdam, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stärk, R.F. (1990). A quantifier-free completion of logic programs. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '89. CSL 1989. Lecture Notes in Computer Science, vol 440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52753-2_53
Download citation
DOI: https://doi.org/10.1007/3-540-52753-2_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52753-4
Online ISBN: 978-3-540-47137-0
eBook Packages: Springer Book Archive