Abstract
We investigate Negation as Failure as incorporated in (nondeterministic) SLDNF-resolution and in (deterministic) PROLOG's resolution. We formulate three Gentzen-style systems which characterize prepositional SLDNF-resolution and propositional PROLOG's resolution in a sound and complete way (without assuming stratification or any other restrictions on programs.) Our analysis employs certain three-valued logics.
The results of this paper can be of interest for rule-based expert systems which represent knowledge in propositional logic, and for other AI-systems which use Negation as Failure for non-monotonic reasoning.
This research has been supported from the University of Miami's Summer '92 Award in Natural Sciences and Engineering
Preview
Unable to display preview. Download preview PDF.
References
K. R. Apt, Introduction to Logic Programming, in J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, North Holland, 1989.
K. R. Apt, H. A. Blair and A. Walker, Towards a Theory of Declarative knowledge, in [28], pp. 89–48.
K. R. Apt and M. H. Van Emden, Contributions to the Theory of Logic Programming, J. ACM 29, 3, July 1982, pp. 841–862.
L. Cavedon and J. W. Lloyd, A Completeness Theorem for SLDNF Resolution, Journal of logic programming, 1989, vol. 7, No 3, pp. 177–192.
D. Chan, Constructive Negation Based on Completed Database, in [20], pp. 111–125.
K. L. Clark, Negation as Failure, in Logic and Databases, H. Gallaire and J. Minker (eds.), Plenum Press, New York, 1978, 193–322.
K. L. Clark, Predicate Logic as a Computational Formalism, Research Report DOC 79/59, Dept. of Computing, Imperial College, 1979.
P. M. Dung and K. Kanchanasut, On the Generalized Predicate Completion of Non-Horn Programs, in [27], pp. 587–603.
P. M. Dung and K. Kanchanasut, A Fixpoint Approach to Declarative Semantics of Logic Programs, in [27], pp. 604–625.
M. Falaschi, G. Levi, M. Martelli, C. Palamidessi, A New Declarative Semantics for Logic Languages, in [20], pp. 993–1005.
M. Fitting, A Kripke-Kleene Semantics for Logic Programs, Journal of Logic Programming, 1985, No 4, pp 295–312.
M. Fitting, Partial Models and Logic Programming, Journal of Theoretical Computer Science 48 (1986), pp. 229–255.
M. Fitting and M. Ben Jacob, Stratified and Three-valued Logic Programming Semantics, in [20], pp. 1054–1069.
D. Gabbay, Modal Provability Foundations for Negation as Failure I, 4th draft, Feb 1989, unpublished.
M. Gelfond and V. Lifschitz, The Stable Model Semantics for Logic Programming, in [20], pp. 1070–1080.
J. Harland, A Kripke-like Model for Negation as Failure, in [27], pp 626–644. J. Jaffar, J.-L. Lassez and J. W. Lloyd, Completeness of the negation as failure rule, IJCAI-83, Karlsruhe, 1983, pp. 500–506.
R. A. Kowalski, Predicate Logic as a Programming Language, Information Processing '74, Stockholm, North Holland, 1974, pp. 569–574.
R. A. Kowalski, Algorithm = Logic + Control, Communications of the ACM 22, 7, July 1979, pp. 424–436.
R. A. Kowalski, The Relation Between Logic Progamming and Logic Specification, in C. A. R. Hoare and J. C. Shepherdson (eds.) Mathematical Logic and Programming Languages, Prentice Hall, Englewood Cliffs, N.J. 1985, pp. 11–27.
R. A. Kowalski and K. A. Bowen (eds.), Logic Programming, Proceedings of the Fifth International Conference and Symposium, MIT Press, 1988.
K. Kunen, Some Remarks on the Completed Database, in [20], pp. 978–992.
K. Kunen, Negation in Logic Programming, Journal of logic programming 1987, No 4, pp 289–308.
K. Kunen, Signed Data Dependencies in Logic Programs, Journal of logic programming, 1989, vol. 7, No 3, pp.231–247.
G. Levi and M. Martelli (eds.), Logic Programming, Proceedings of the Sixth International Conference, MIT Press, 1989.
V. Lifschitz, On the Declarative Semantics of Logic Programs with Negation, in [28], pp. 177–192.
J. W. Lloyd, Foundations of Logic Programming, Second extended edition, Springer Verlag, 1987.
E. L. Lusk and R. A. Overbeek (eds.), Logic Programming, Proceedings of the North American Conference 1989, MIT Press, 1989.
J. Minker (ed.), Foundations of Deductive Databases and Logic Programming, Morgan Kaufmann, 1988.
D. Pearce and G. Wagner, Reasoning with Negative Information I: Strong negation in Logic Programs, draft 1989.
J. A. Plaza, Fully Declarative Programming with Logic—Mathematical Foundations, Ph.D. Dissertation, City University of New York, July 1990.
J. A. Plaza, Completeness for Propositional Logic Programs with Negation, in: Z.W. Ras and M. Zemankowa (eds.), Methodologies for Intelligent Systems — Proceedings of the 6th International Symposium 1991, Lecture Notes in Artificial Intelligence 542, Springer Verlag, 1991.
H. Przymusińska and T. Przymusiński, Weakly Perfect Model Semantics for Logic Programs, in [20], pp. 1106–1123.
T. C. Przymusiński, On the Declarative Semantics of Deductive Databases and Logic Programs, in [28], pp. 193–216.
T. C. Przymusiński, On Constructive Negation in Logic Programming, in [27], addendum.
T. C. Przymusiński, On the Declarative and Procedural Semantics of Logic Programs, to appear in Journal of Logic Programming.
J. C. Shepherdson, Negation in Logic Programming, in [28], pp. 19–88.
J. R. Shoenfield, Mathematical Logic, Addison-Wesley, 1967.
L. Sterling and E. Shapiro, The Art of PROLOG, MIT Press, 1986.
M. Wallace, A Computable Semantics for General Logic Programs, Journal of Logic Programming 1989, vol. 6, No 3, pp. 269–297.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Plaza, J.A. (1993). Gentzen-style characterizations of Negation as Failure. In: Calmet, J., Campbell, J.A. (eds) Artificial Intelligence and Symbolic Mathematical Computing. AISMC 1992. Lecture Notes in Computer Science, vol 737. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57322-4_17
Download citation
DOI: https://doi.org/10.1007/3-540-57322-4_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57322-7
Online ISBN: 978-3-540-48063-1
eBook Packages: Springer Book Archive