Abstract
A characterisation of a logic programming system is given in the form of a natural deduction proof system. The proof system is proven to be “equivalent” to an operational semantics for the logic programming system, in the sense that the set of theorems of the proof system is exactly the set of existential closures of queries solvable in the operational semantics. It is argued that this proof-theoretic characterisation captures our intuitions about logic programming better than do traditional characterisations, such as those using resolution or fixpoint semantics.
Preview
Unable to display preview. Download preview PDF.
References
James H. Andrews. Proof-theoretic characterisations of logic programming. Technical Report LFCS-89-77, Laboratory for the Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, May 1989.
K. L. Clark. Negation as failure. In Logic and Data Bases, pages 293–322, New York, 1978. Plenum Press.
K. L. Clark. Predicate logic as a computational formalism. Technical Report 79/59 TOC, Department of Computing, Imperial College, London, December 1979.
Gerhardt Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969. Ed. M. E. Szabo.
John W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1984.
Per Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium. North-Holland, 1971.
Gordon Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, September 1981.
Raymond M. Smullyan. First-Order Logic. Springer-Verlag, Berlin, 1968.
Göran Sundholm. Systems of deduction. In D. Gabbay and F. Guenther, editors, Handbook of Philosophical Logic, pages 133–188. D. Reidel, Dordrecht, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andrews, J.H. (1989). Proof-theoretic characterisations of logic programming. In: Kreczmar, A., Mirkowska, G. (eds) Mathematical Foundations of Computer Science 1989. MFCS 1989. Lecture Notes in Computer Science, vol 379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51486-4_62
Download citation
DOI: https://doi.org/10.1007/3-540-51486-4_62
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51486-2
Online ISBN: 978-3-540-48176-8
eBook Packages: Springer Book Archive