Advertisement

Logics for Negation as Failure

  • J. C. Shepherdson
Conference paper
Part of the Mathematical Sciences Research Institute Publications book series (MSRI, volume 21)

Abstract

Negation as failure is the version of negation commonly used in logic programming. It decrees that a (ground) goal A succeeds if A fails and fails if A succeeds. It is not sound with respect to the straightforward classical reading of a program. This paper surveys the ways in which different types of logic—classical two-valued, three-valued, intuitionistic, modal, autoepistemic, linear—have been used to provide declarative semantics for negation as failure.

Keywords

Logic Program Logic Programming Function Symbol Predicate Symbol Ground Atom 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Apt, K. R. and Blair, H. A. [1988], Arithmetic classification of perfect models of stratified programs, Report TR-88–09, University of Texas at Austin.Google Scholar
  2. 2.
    Apt, K. R.; Blair, H. A. and Walker, A. [1988], Towards a theory of declarative knowledge, in “Foundations of Deductive Databases and Logic Programming”, (J. Minker, Ed.), Morgan Kaufmann, Los Altos, CA, 89–148.Google Scholar
  3. 3.
    Apt. K. R. and Pugin, J.-M. [1987], Management of stratified databases, Report TR-87–41, University of Texas at Austin.Google Scholar
  4. 4.
    Apt, K. R. and Emden, M. H. van [1982], Contributions to the theory of logic programming, JACM 29, 841–863.CrossRefMATHGoogle Scholar
  5. 5.
    Barbuti, R. and Martelli, M. [1986], Completeness of SLDNF-resolution for structured programs, submitted to Theoretical Computer Science 21.Google Scholar
  6. 6.
    Blair, H. A. [1982], The recursion theoretic complexity of the semantics of predicate logic as a programming language, Information and Control 54, 25–47.MathSciNetCrossRefMATHGoogle Scholar
  7. 7.
    . Blair, H. A. [1986], Decidability in the Herbrand base, in “Proceedings Workshop on Foundations of Deductive Databases and Logic Programming”, (J. Minker, Ed.), Washington, DC.Google Scholar
  8. 8.
    Börger, E. [1987], Unsolvable decision problems for PROLOG programs, to appear in Computer Theory and Logic (E. Börger, Ed.), Lecture Notes in Computer Science, Springer-Verlag.Google Scholar
  9. 9.
    Brass, S. and Lipeck, U. W. [1989], Specifying closed world assumptions for logic databases, Proc. Second Symposium on Mathematical Fundamentals of Database Systems (MFDBS89).Google Scholar
  10. 10.
    Cavedon, L. [1988], On the completeness of SLDNF-resolution, Ph.D. Thesis, Melbourne University, 120.Google Scholar
  11. 11.
    Cavedon, L. and Lloyd, J. W. [1989], A completeness theorem for SLDNF-resolution, J. Logic Programming 7(3), 177–192.MathSciNetCrossRefMATHGoogle Scholar
  12. 12.
    Carvalho, R. L.; de Maibaum, T. S. E.; Pequeno, T. H. C.; Pereda, A. A. and Veloso, P. A. S. [1980], A model theoretic approach to the theory of abstract data types and structures, Research Report CS-80–22, Waterloo, Ontario.Google Scholar
  13. 13.
    Cerrito, S., Negation as failure, a linear axiomatization, to appear in J. Logic Programming.Google Scholar
  14. 14.
    Chan, D. [1988], Constructive negation based on the completed database, Proc. 1988 Conference and Symposium on Logic Programming, Seattle, Washington, September 1988, pp. 111–125.Google Scholar
  15. 15.
    Clark, K. L. [1978], Negation as failure, in “Logic and Data Base” (H. Gallaire and J. Minker, Eds.), Plenum, New York, 293–322.Google Scholar
  16. 15.
    Davis, M. [1983], The prehistory and early history of automated deduction, in “Automation of Reasoning” (J. Siekmann and G. Wrightson, Eds.), Springer, Berlin, Vol. (1983), 1–28.Google Scholar
  17. 17.
    Ebbinghaus, H. D. [1969], Über eine prädikaten logik mit partiell definierten prädikat-en and funktionen, Arch. Math. Logik 12, 39–53.MathSciNetCrossRefMATHGoogle Scholar
  18. 18.
    Fine, K. [1989], The justification of negation as failure, Logic, Methodology and Philosophy of Science VIII (J. E. Fenstad et al., Eds.) Elsevier Science Publishers B.V.Google Scholar
  19. 19.
    Fitting, M. [1985], A Kripke-Kleene semantics for general logic programs, Logic Programming 2, 295–312.MathSciNetCrossRefMATHGoogle Scholar
  20. 20.
    Fitting, M. [1986], Partial models and logic programming, to appear in Computer Science.Google Scholar
  21. 21.
    Fitting, M. [1987a], Pseudo-boolean valued Prolog, Research Report, H. Lehman College, (CUNY), Bronx, NY.Google Scholar
  22. 22.
    Fitting, M. [1987b], Logic programming on a topological bilattice, Research Report, H. Lehman College, (CUNY), Bronx, NY.Google Scholar
  23. 23.
    Fitting, M. [1988b], Bilattices and the semantics of logic programming, Research Report, Dept. of Computer Science, CUNY.Google Scholar
  24. 24.
    Fitting, M. and Ben-Jacob, M. [1988], Stratified and three-valued logic programming semantics, Research Report, Dept. of Computer Science, CUNY.Google Scholar
  25. 25.
    Gabbay, D. M. [1985], N-Prolog: An extension of Prolog with hypothetical implication, II. Logical Foundations, and Negations as Failure, J. Log. Programming 2(4), 251–283.MathSciNetCrossRefMATHGoogle Scholar
  26. 26.
    Gabbay, D. M. [1989], Modal provability foundations for negation by failure, Preprint.Google Scholar
  27. 27.
    Gabbay, D. M. and Sergot, M. J. [1986], Negation as inconsistency, J. Logic Programming 3(1), 1–36.MathSciNetCrossRefMATHGoogle Scholar
  28. 28.
    Gallier, J. H. and Raatz, S. [1986a], HORNLOG: A graph based interpreter for general Horn clauses, Technical Report MS-CIS-86–10, University of Pennsylvania; J. Logic Programming 4 2, 119–156.MathSciNetCrossRefGoogle Scholar
  29. 29.
    Gallier, J. H. and Raatz, S. [1986b], Extending SLD-resolution to equational Horn clauses using E-unification, J. Logic Programming 6, 3–44, Short version to appear, 1986 IEEE Symposium on Logic Programming, Salt Lake City, UT.MathSciNetCrossRefGoogle Scholar
  30. 30.
    Gelfond, M. [1987], On stratified autoepistemic theories, in “Proceedings AAAI-87”, 207–211, American Association for Artificial Intelligence, Morgan Kaufmann, Los Altos, CA.Google Scholar
  31. 31.
    Gelfond, M. and Lifschitz, V. [1988], The stable model semantics for logic programming, 5th International Conference on Logic Programming, Seattle.Google Scholar
  32. 32.
    Gelfond, M.; Przymusinski, H. and Przymusinski, T. [1986],The extended closed world assumption and its relationship to parallel circumscription, Proceedings ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, Cambridge, MA, 133–139.Google Scholar
  33. 33.
    Gelfond, M.; Przymusinski, H. and Przymusinski, T. [1986a], On the relationship between circumscription and negation as failure, to appear in Artificial Intelligence.Google Scholar
  34. 34.
    Girard, J. Y. [1987], Linear logic, Theoretical Computer Science 50.Google Scholar
  35. 35.
    Goguen, J. A. and Burstall, R. M. [1984], Institutions: Abstract model theory for computer science, Proc. of Logic Programming Workshop (E. Clark and D. Kozen, Eds.), Lecture Notes in Computer Science 164, Springer-Verlag, 221–256.Google Scholar
  36. 36.
    Haken, A. [1985], The intractability of resolution, Theoretical Computer Science 39, 297–308.MathSciNetCrossRefMATHGoogle Scholar
  37. 37.
    Henschen, L. J. and Park, H.-S. [1988], Compiling the GCWA in indefinite databases, in “Foundations of Deductive Databases and Logic Programming” (J. Minker, Ed.), Morgan Kaufmann Publishers, Los Altos, CA, 395–438.Google Scholar
  38. 38.
    Hodges, W. [1985], The logical basis of PROLOG, unpublished text of lecture, 1–10.Google Scholar
  39. 39.
    Jäger, G. [1988], Annotations on the consistency of the closed world assumption, Preprint, Computer Science Dept., Technische Hochschule, Zürich (1987).Google Scholar
  40. 40.
    Jaffar, J.; Lassez, J.-L. and Lloyd, J. W. [1983], Completeness of the negation as failure rule, IJCAI-83, Karlsruhe, 500–506. Google Scholar
  41. 41.
    Jaffar, J.; Lassez, J.-L. and Mäher, M. J. [1984a], A theory of complete logic programs with equality, J. Logic Programming 1(3), 211–223.MathSciNetCrossRefMATHGoogle Scholar
  42. 42.
    Jaffar, J.; Lassez, J.-L. and Mäher, M. J. [1984b], A logic programming language scheme, in “Logic Programming Relations, Functions and Equations” (D. DeGroot and G. Lindstrom, Eds.), Prentice Hall. Also Technical Report TR 84/15, University of Melbourne.Google Scholar
  43. 43.
    Jaffar, J.; Lassez, J.-L. and Mäher, M. J. [1986a], Comments onGeneral Failure of Logic Programs”, J. Logic Programming 3(2), 115–118.MathSciNetCrossRefMATHGoogle Scholar
  44. 44.
    Jaffar, J.; Lassez, J.-L. and Maner, M. J. [1986b], Some issues and trends in the semantics of logic programs, Proceedings Third International Conference on Logic Programming, Springer, 223–241.Google Scholar
  45. 45.
    Jaffar, J. and Stuckey, P. J. [1986], Canonical logic programs, J. Logic Programming 3, 143–155.MathSciNetCrossRefMATHGoogle Scholar
  46. 46.
    Kleene, S. C. [1952], Introduction to Metamathematics, van Nostrand, New York.MATHGoogle Scholar
  47. 47.
    Kowalski, R. [1979], Logic for Problem Solving, North Holland, New York.MATHGoogle Scholar
  48. 48.
    Kunen, K. [1987], Negation in logic programming, J. Logic Programming 4, 289–308.MathSciNetCrossRefMATHGoogle Scholar
  49. 49.
    Kunen, K. [1987a], Signed data dependencies in logic programs, Computer Sciences Technical Report #719, University of Wisconsin, Madison. Also J. Logic Programming 7(3), 231–246.MathSciNetCrossRefGoogle Scholar
  50. 50.
    Lassez, J.-L. and Mäher, M. J. [1984], Closures and fairness in the semantics of programming logic, Theoretical Computer Science 29, 167–184.MathSciNetCrossRefGoogle Scholar
  51. 51.
    Lassez, J.-L. and Mäher, M. J. [1985], Optimal fixed points of logic programs, Theoretical Computer Science 39, 15–25.MathSciNetCrossRefMATHGoogle Scholar
  52. 52.
    Lewis, H. [1978],Renaming a set of clauses as a Horn set, JACM 25, 134–135.CrossRefMATHGoogle Scholar
  53. 53.
    Lifschitz, V. [1985], Renaming a set of clauses as a Horn setComputing circumscription, Proceedings IJCAI-85m, 121–127.Google Scholar
  54. 54.
    Lifschitz, V. [1988], On the declarative semantics of logic programs with negation, Foundations of Deductive Databases and Logic Programming (J. Minker, Ed.), Morgan Kaufmann Publishers, Los Altos, CA, 177–192.Google Scholar
  55. 55.
    Lloyd, J. W. [1987], Foundations of Logic Programming, 2nd edition Springer, Berlin.MATHGoogle Scholar
  56. 56.
    Lloyd, J. W. and Topor, R. W. [1984], Making PROLOG more expressive, J. Logic Programming 1, 225–240.MathSciNetCrossRefMATHGoogle Scholar
  57. 57.
    Lloyd, J. W. and Topor, R. W. [1985], A basis for deductive data base systems, II, J. Logic Programming 3, 55–68.MathSciNetCrossRefGoogle Scholar
  58. 58.
    Loveland, D. W. [1988], Near-Horn Prolog, Proc. ICLP’87, (J.-L. Lassez, Ed.), MIT Press.Google Scholar
  59. 59.
    McCarthy, J. [1984], Applications of circumscription to formalizing common sense knowledge, A A AI Workshop on Non-Monotonic Reasoning, 295–323.Google Scholar
  60. 60.
    Mäher, M. J. [1987], Complete axiomatization of the algebras of finite, infinite and rational trees, Technical Report, IBM T. J. Watson Research Centre, Yorktown Heights, NY.Google Scholar
  61. 61.
    Mahr, B. and Makowsky, J. A. [1983], Characterizing specification langauges which admit initial semantics, Proc. 8th CAAP, Lecture Notes in Computer Science 159, Springer-Verlag, 300–316.Google Scholar
  62. 62.
    Makowsky, J. A. [1986], Why Horn formulas matter in computer science: Initial structures and generic examples, Technical Report No. 329, Technion Haifa, 1984 (extended abstract); in Mathematical Foundations of Software Development, Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT) (H. Ehrig et al., Eds.), Lecture Notes in Computer Science 185, Springer (1985), 374–387, and (revised version) May 15, 1986, 1–28, preprint. The references in the text are to this most recent version.Google Scholar
  63. 63.
    Malcev, A. [1971], Axiomatizable classes of locally free algebras of various types, in “The Metamathematics of Algebraic Systems: Collected Papers”, Chapter 23, 262–281, North Holland, Amsterdam.Google Scholar
  64. 64.
    Meitzer, B. [1983], Theorem-proving for computers: Some results on resolution and renaming, in “Automation of Reasoning”, 1 (J. Siekmann and G. Wrightson, Eds.), Springer, Berlin, 493–495.Google Scholar
  65. 65.
    Minker, J. [1982], On indefinite data bases and the closed world assumption, Proc. 6th Conf. Automated Deduction, Lecture Notes in Computer Science 138, Springer-Verlag, 292–308.Google Scholar
  66. 66.
    Minker, J. and Perlis, D. [1985], Computing protected circumscription, J. Logic Programming 2, 1–24.MathSciNetCrossRefGoogle Scholar
  67. 67.
    Mints, G. [1986], Complete calculus for pure Prolog (Russian), Proc. Acad. Sei. Estonian SSR, 35, 4, 367–380.MathSciNetMATHGoogle Scholar
  68. 68.
    Mints, G. [1990], Several Formal Systems of the Logic Programming, Computer and Artificial Intelligence 9, 19–41.MathSciNetMATHGoogle Scholar
  69. 69.
    Moore, R. C. [1985], Semantic considerations on non-monotonic logic, Artificial Intelligence 25, 75–94.MathSciNetCrossRefMATHGoogle Scholar
  70. 70.
    Mycroft, A. [1983], Logic programs and many-valued logic, Proc. 1st STACS Conference.Google Scholar
  71. 71.
    Naish, L. [1986], Negation and quantifiers in NU-Prolog, Proceedings Third International Conference on Logic Programming, Springer, 624–634.Google Scholar
  72. 72.
    Naqvi, S. A. [1986], A logic for negation in database systems, in “Proceedings of Workshop on Foundations of Deductive Databases and Logic Programming”, (J. Minker, Ed.), Washington, DC.Google Scholar
  73. 73.
    Plaisted, D. A. [1984], Complete problems in the first-order predicate calculus, J. Comp. System Sciences 29, 8–35.MathSciNetCrossRefMATHGoogle Scholar
  74. 74.
    Poole, D. L. and Goebel, R. [1986], Gracefully adding negation and disjunction to Prolog, Proceedings Third International Conference on Logic Programming, Springer, 635–641.Google Scholar
  75. 75.
    Przymusinska, H. [1987], On the relationship between autoepistemic logic and circumscription for stratified deductive databases, Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems, Knoxville, Tenn.Google Scholar
  76. 76.
    Przymusinska, H. and Przymusinski, T. [1988], Weakly perfect model semantics for logic programs, In R. Kowalski and K. Bowen, Editors, Proceedings of the Fifth Logic Programming Symposium, 1106–1122, Association for Logic Programming, MIT Press, Cambridge, Mass.Google Scholar
  77. 77.
    Przymusinski, T. C. [1988], On the semantics of stratified deductive databases, in “Foundations of Deductive Database and Logic Programming” (J. Minker, Ed.), Morgan Kaufmann Publishers, Los Altos, CA, 193–216.Google Scholar
  78. 78.
    Przymusinski, T. C. [1988a], On the declarative and procedural semantics of logic programs, J. Automated Reasoning, 4. In print. (Extended abstract appeared in: Przymusinski, T. C. [1988] Perfect model semantics. In R. Kowalski and K. Bowen, Editors, Proceedings of the Fifth Logic Programming Symposium, 1081–1096, Assocaition for Logic Programming, MIT Press, Cambridge, Mass.Google Scholar
  79. 79.
    Przymusinski, T. C. [1988b], On constructive negation in logic programming, Technical Report Draft, University of Texas at El Paso.Google Scholar
  80. 80.
    Przymusinski, T. C. [1988c], Three-valued formalizations of non-monotonic reasoning and logic programming, Research Report, Dept. of Mathematics, University of Texas at El Paso.Google Scholar
  81. 81.
    Przymusinski, T. C. [1989], Three-valued stable semantics for normal and disjunctive logic programs, Technical Report, University of Texas at El Paso.Google Scholar
  82. 82.
    Przymusinski, T. C. [1989], Three-valued non-monotonic formalisms and logic programming, in “Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning (KR’89)”, Toronto, Canada. In print. Google Scholar
  83. 83.
    Reiter, R. [1978], On closed world data bases, in “Logic and Data Bases” (H. Gallaire and J. Minker, Eds.), Plenum, New York, 55–76.Google Scholar
  84. 84.
    Reynolds, M. [1987], The expressive power of query languages based on logic programming, Ph.D. Thesis, University London.Google Scholar
  85. 85.
    Reynolds, M. [1987a], A completeness result for logic programming, Manuscript.Google Scholar
  86. 86.
    Reynolds, M. [1988], Declarative meaning for logic programs with negation as failure, Manuscript.Google Scholar
  87. 87.
    Ross, K. [1989], A procedural semantics for well-founded negation in logic programs, in “Proceedings of the Eighth Symposium on Principles of Database Systems”, ACM SIGACT-SIGMOD.Google Scholar
  88. 88.
    Ross, K. and Topor. R. W. [1987], Inferring negative information from disjunctive databases, Technical Report 87/1, University of Melbourne.Google Scholar
  89. 89.
    Sakai, K. and Miyachi, T. [1983], Incorporating naive negation into PROLOG, ICOT Technical Report: TR-028.Google Scholar
  90. 90.
    Sato, T. [1982], Negation and semantics of PROLOG programs, Proc. 1st International Conference on Logic Programming, 169–174.Google Scholar
  91. 91.
    Sato, T. [1987], On the consistency of first order logic programs, Tech. Report 87–12, Electrotechnical Laboratory, Ibarki, Japan.Google Scholar
  92. 92.
    Sato, T. [1988], Completed logic programs and their consistency, Typescript, Electrotechnical Laboratory, Ibaraki, Japan. To appear in J. Logic Programming.Google Scholar
  93. 93.
    Schmitt, P. H. [1986], Computational aspects of three-valued logic, Proc. 8th Conf. Automated Deduction, Lecture Notes in Computer Science, 230, Springer-Verlag, 190–198.Google Scholar
  94. 94.
    Shepherdson, J. C. [1984], Negation as failure: A comparison of Clark’s completed data base and Reiter’s closed world assumption, J. Logic Programming 1, 51–81.MathSciNetCrossRefMATHGoogle Scholar
  95. 95.
    Shepherdson, J. C. [1985], Negation as failure II, J. Logic Programming 3, 185–202.MathSciNetCrossRefGoogle Scholar
  96. 96.
    Shepherdson, J. C. [1988], Negation in logic programming, in “Foundations of Deductive Databases and Logic Programming” (J. Minker, Ed.), Morgan Kaufmann, Los Altos, CA, 19–88.Google Scholar
  97. 97.
    Shepherdson, J. C. [1988a], Language and equality theory in logic programming, Technical Report PM-88–08, Mathematics Dept., Univ. Bristol, 1–41.Google Scholar
  98. 98.
    Shepherdson, J. C. [1988b], SLDNF-resolution with equality, Technical Report PM-88–05, Mathematics Dept., Univ. Bristol, 1–15; Journal of Automated Reasoning 6 (1990). Google Scholar
  99. 99.
    Shepherdson, J. C. [1989], Unsolvable problems for SLDNF-resolution, J. Logic Programming 10, 19–22.MathSciNetCrossRefGoogle Scholar
  100. 100.
    Shepherdson, J. C. [1989a], A sound and complete semantics for a version of negation as failure, Theoretical Computer Science 65, 343–371.MathSciNetCrossRefMATHGoogle Scholar
  101. 101.
    Shepherdson, J. C. [1989b], Mints type deductive calculi for logic programming, Technical Report, Mathematics Dept., University of Bristol, to appear in special issue of Annals of Pure and Applied Logic in memory of John Myhill.Google Scholar
  102. 102.
    Solovay, R. M. [1976], Provability interpretation of modal logic, Israel Journal of Mathematics 25, 287–304.MathSciNetCrossRefMATHGoogle Scholar
  103. 103.
    Stickel, M. E. [1986], A PROLOG technology theorem prover: Implementation by an extended PROLOG compiler, Proceedings Eighth International Conference on Automated Deduction, Springer, 573–587.Google Scholar
  104. 104.
    Terracini, L. [1988], Modal interpretation for negation by failure, Atti delPAcademia delle Scienze di Torino 122, 81–88.MathSciNetMATHGoogle Scholar
  105. 105.
    Terracini, L. [1988a], A complete bi-modal system for a class of models, Atti dellAca-demia delle Scienze di Torino 122, 116–125.MathSciNetMATHGoogle Scholar
  106. 106.
    Van Gelder, A. [1988], Negation as failure using tight derivations for general logic programs, Foundations of Deductive Databases and Logic Programming (J. Minker, Ed.), Morgan Kaufmann Publishers, Los Altos, CA, 149–176; revised version in J. Logic Programming 6, 109–133, 1989.Google Scholar
  107. 107.
    Van Gelder, A.; Ross, K. and Schlipf [1988], Unfounded sets and well-founded semantics for general logic programs, in “Proceedings of the Symposium on Principles of Database Systems”, ACM SIGACT-SIGMOD.Google Scholar
  108. 108.
    Voda, P. J. [1986], Choices in, and limitations of, logic programming, Proc. 3rd Int. Conf. Logic Programming, Springer, 615–623.Google Scholar
  109. 109.
    Yahya, A. and Henschen, L. [1985], Deduction in non-Horn databases, J. Automated Reasoning 1(2), 141–160.MathSciNetCrossRefMATHGoogle Scholar

Copyright information

© Springer-Verlag New York, Inc 1992

Authors and Affiliations

  • J. C. Shepherdson
    • 1
    • 2
  1. 1.Mathematics DepartmentUniversity of BristolEngland
  2. 2.Mathematical Science Research InstituteBerkeleyUSA

Personalised recommendations