Skip to main content

Gentzen-style characterizations of Negation as Failure

  • Conference paper
  • First Online:
  • 166 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 737))

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

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. R. Apt, Introduction to Logic Programming, in J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, North Holland, 1989.

    Google Scholar 

  2. K. R. Apt, H. A. Blair and A. Walker, Towards a Theory of Declarative knowledge, in [28], pp. 89–48.

    Google Scholar 

  3. K. R. Apt and M. H. Van Emden, Contributions to the Theory of Logic Programming, J. ACM 29, 3, July 1982, pp. 841–862.

    Google Scholar 

  4. L. Cavedon and J. W. Lloyd, A Completeness Theorem for SLDNF Resolution, Journal of logic programming, 1989, vol. 7, No 3, pp. 177–192.

    Google Scholar 

  5. D. Chan, Constructive Negation Based on Completed Database, in [20], pp. 111–125.

    Google Scholar 

  6. K. L. Clark, Negation as Failure, in Logic and Databases, H. Gallaire and J. Minker (eds.), Plenum Press, New York, 1978, 193–322.

    Google Scholar 

  7. K. L. Clark, Predicate Logic as a Computational Formalism, Research Report DOC 79/59, Dept. of Computing, Imperial College, 1979.

    Google Scholar 

  8. P. M. Dung and K. Kanchanasut, On the Generalized Predicate Completion of Non-Horn Programs, in [27], pp. 587–603.

    Google Scholar 

  9. P. M. Dung and K. Kanchanasut, A Fixpoint Approach to Declarative Semantics of Logic Programs, in [27], pp. 604–625.

    Google Scholar 

  10. M. Falaschi, G. Levi, M. Martelli, C. Palamidessi, A New Declarative Semantics for Logic Languages, in [20], pp. 993–1005.

    Google Scholar 

  11. M. Fitting, A Kripke-Kleene Semantics for Logic Programs, Journal of Logic Programming, 1985, No 4, pp 295–312.

    Google Scholar 

  12. M. Fitting, Partial Models and Logic Programming, Journal of Theoretical Computer Science 48 (1986), pp. 229–255.

    Google Scholar 

  13. M. Fitting and M. Ben Jacob, Stratified and Three-valued Logic Programming Semantics, in [20], pp. 1054–1069.

    Google Scholar 

  14. D. Gabbay, Modal Provability Foundations for Negation as Failure I, 4th draft, Feb 1989, unpublished.

    Google Scholar 

  15. M. Gelfond and V. Lifschitz, The Stable Model Semantics for Logic Programming, in [20], pp. 1070–1080.

    Google Scholar 

  16. 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.

    Google Scholar 

  17. R. A. Kowalski, Predicate Logic as a Programming Language, Information Processing '74, Stockholm, North Holland, 1974, pp. 569–574.

    Google Scholar 

  18. R. A. Kowalski, Algorithm = Logic + Control, Communications of the ACM 22, 7, July 1979, pp. 424–436.

    Google Scholar 

  19. 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.

    Google Scholar 

  20. R. A. Kowalski and K. A. Bowen (eds.), Logic Programming, Proceedings of the Fifth International Conference and Symposium, MIT Press, 1988.

    Google Scholar 

  21. K. Kunen, Some Remarks on the Completed Database, in [20], pp. 978–992.

    Google Scholar 

  22. K. Kunen, Negation in Logic Programming, Journal of logic programming 1987, No 4, pp 289–308.

    Google Scholar 

  23. K. Kunen, Signed Data Dependencies in Logic Programs, Journal of logic programming, 1989, vol. 7, No 3, pp.231–247.

    Google Scholar 

  24. G. Levi and M. Martelli (eds.), Logic Programming, Proceedings of the Sixth International Conference, MIT Press, 1989.

    Google Scholar 

  25. V. Lifschitz, On the Declarative Semantics of Logic Programs with Negation, in [28], pp. 177–192.

    Google Scholar 

  26. J. W. Lloyd, Foundations of Logic Programming, Second extended edition, Springer Verlag, 1987.

    Google Scholar 

  27. E. L. Lusk and R. A. Overbeek (eds.), Logic Programming, Proceedings of the North American Conference 1989, MIT Press, 1989.

    Google Scholar 

  28. J. Minker (ed.), Foundations of Deductive Databases and Logic Programming, Morgan Kaufmann, 1988.

    Google Scholar 

  29. D. Pearce and G. Wagner, Reasoning with Negative Information I: Strong negation in Logic Programs, draft 1989.

    Google Scholar 

  30. J. A. Plaza, Fully Declarative Programming with Logic—Mathematical Foundations, Ph.D. Dissertation, City University of New York, July 1990.

    Google Scholar 

  31. 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.

    Google Scholar 

  32. H. Przymusińska and T. Przymusiński, Weakly Perfect Model Semantics for Logic Programs, in [20], pp. 1106–1123.

    Google Scholar 

  33. T. C. Przymusiński, On the Declarative Semantics of Deductive Databases and Logic Programs, in [28], pp. 193–216.

    Google Scholar 

  34. T. C. Przymusiński, On Constructive Negation in Logic Programming, in [27], addendum.

    Google Scholar 

  35. T. C. Przymusiński, On the Declarative and Procedural Semantics of Logic Programs, to appear in Journal of Logic Programming.

    Google Scholar 

  36. J. C. Shepherdson, Negation in Logic Programming, in [28], pp. 19–88.

    Google Scholar 

  37. J. R. Shoenfield, Mathematical Logic, Addison-Wesley, 1967.

    Google Scholar 

  38. L. Sterling and E. Shapiro, The Art of PROLOG, MIT Press, 1986.

    Google Scholar 

  39. M. Wallace, A Computable Semantics for General Logic Programs, Journal of Logic Programming 1989, vol. 6, No 3, pp. 269–297.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Jacques Calmet John A. Campbell

Rights and permissions

Reprints 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

Publish with us

Policies and ethics