Logic from Computer Science pp 521-583 | Cite as

# Logics for Negation as Failure

Conference paper

## 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

Stratification Posit Plague## Preview

Unable to display preview. Download preview PDF.

### References

- 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.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.Apt. K. R. and Pugin, J.-M. [1987],
*Management of stratified databases*, Report TR-87–41, University of Texas at Austin.Google Scholar - 4.Apt, K. R. and Emden, M. H. van [1982],
*Contributions to the theory of logic programming*, JACM**29**, 841–863.CrossRefMATHGoogle Scholar - 5.Barbuti, R. and Martelli, M. [1986],
*Completeness of*SLDNF-*resolution for structured programs*, submitted to Theoretical Computer Science**21**.Google Scholar - 6.Blair, H. A. [1982], T
*he recursion theoretic complexity of the semantics of predicate logic as a programming language*, Information and Control**54**, 25–47.MathSciNetCrossRefMATHGoogle Scholar - 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.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.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.Cavedon, L. [1988],
*On the completeness of*SLDNF-*resolution*, Ph.D. Thesis, Melbourne University, 120.Google Scholar - 11.Cavedon, L. and Lloyd, J. W. [1989],
*A completeness theorem for*SLDNF-*resolution*, J. Logic Programming 7(3), 177–192.MathSciNetCrossRefMATHGoogle Scholar - 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.Cerrito, S.,
*Negation as failure, a linear axiomatization*, to appear in J. Logic Programming.Google Scholar - 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.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 - 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.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.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.Fitting, M. [1985],
*A Kripke-Kleene semantics for general logic programs*, Logic Programming 2, 295–312.MathSciNetCrossRefMATHGoogle Scholar - 20.Fitting, M. [1986],
*Partial models and logic programming*, to appear in Computer Science.Google Scholar - 21.Fitting, M. [1987a],
*Pseudo-boolean valued Prolog*, Research Report, H. Lehman College, (CUNY), Bronx, NY.Google Scholar - 22.Fitting, M. [1987b],
*Logic programming on a topological bilattice*, Research Report, H. Lehman College, (CUNY), Bronx, NY.Google Scholar - 23.Fitting, M. [1988b],
*Bilattices and the semantics of logic programming*, Research Report, Dept. of Computer Science, CUNY.Google Scholar - 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.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.Gabbay, D. M. [1989],
*Modal provability foundations for negation by failure*, Preprint.Google Scholar - 27.Gabbay, D. M. and Sergot, M. J. [1986],
*Negation as inconsistency*, J. Logic Programming 3(1), 1–36.MathSciNetCrossRefMATHGoogle Scholar - 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.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.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.Gelfond, M. and Lifschitz, V. [1988],
*The stable model semantics for logic programming, 5th International Conference on Logic Programming*, Seattle.Google Scholar - 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.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.
- 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.Haken, A. [1985],
*The intractability of resolution*, Theoretical Computer Science**39**, 297–308.MathSciNetCrossRefMATHGoogle Scholar - 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.Hodges, W. [1985],
*The logical basis of*PROLOG, unpublished text of lecture, 1–10.Google Scholar - 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.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.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.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.Jaffar, J.; Lassez, J.-L. and Mäher, M. J. [1986a],
*Comments on*“*General Failure of Logic Programs*”, J. Logic Programming 3(2), 115–118.MathSciNetCrossRefMATHGoogle Scholar - 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.Jaffar, J. and Stuckey, P. J. [1986],
*Canonical logic programs*, J. Logic Programming 3, 143–155.MathSciNetCrossRefMATHGoogle Scholar - 46.Kleene, S. C. [1952],
*Introduction to Metamathematics*, van Nostrand, New York.MATHGoogle Scholar - 47.Kowalski, R. [1979],
*Logic for Problem Solving*, North Holland, New York.MATHGoogle Scholar - 48.Kunen, K. [1987],
*Negation in logic programming*, J. Logic Programming 4, 289–308.MathSciNetCrossRefMATHGoogle Scholar - 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.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.Lassez, J.-L. and Mäher, M. J. [1985],
*Optimal fixed points of logic programs*, Theoretical Computer Science**39**, 15–25.MathSciNetCrossRefMATHGoogle Scholar - 52.Lewis, H. [1978],
*Renaming a set of clauses as a Horn set*, JACM 25, 134–135.CrossRefMATHGoogle Scholar - 53.Lifschitz, V. [1985],
*Renaming a set of clauses as a Horn set*Computing circumscription, Proceedings IJCAI-85m, 121–127.Google Scholar - 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.Lloyd, J. W. [1987],
*Foundations of Logic Programming*, 2nd edition Springer, Berlin.MATHGoogle Scholar - 56.Lloyd, J. W. and Topor, R. W. [1984],
*Making*PROLOG*more expressive*, J. Logic Programming**1**, 225–240.MathSciNetCrossRefMATHGoogle Scholar - 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.Loveland, D. W. [1988],
*Near-Horn Prolog*, Proc. ICLP’87, (J.-L. Lassez, Ed.), MIT Press.Google Scholar - 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.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.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.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.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.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.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.Minker, J. and Perlis, D. [1985],
*Computing protected circumscription*, J. Logic Programming 2, 1–24.MathSciNetCrossRefGoogle Scholar - 67.Mints, G. [1986],
*Complete calculus for pure Prolog (Russian)*, Proc. Acad. Sei. Estonian SSR, 35, 4, 367–380.MathSciNetMATHGoogle Scholar - 68.Mints, G. [1990],
*Several Formal Systems of the Logic Programming*, Computer and Artificial Intelligence 9, 19–41.MathSciNetMATHGoogle Scholar - 69.Moore, R. C. [1985],
*Semantic considerations on non-monotonic logic*, Artificial Intelligence 25, 75–94.MathSciNetCrossRefMATHGoogle Scholar - 70.Mycroft, A. [1983],
*Logic programs and many-valued logic*, Proc. 1st STACS Conference.Google Scholar - 71.Naish, L. [1986],
*Negation and quantifiers in NU-Prolog*, Proceedings Third International Conference on Logic Programming, Springer, 624–634.Google Scholar - 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.Plaisted, D. A. [1984],
*Complete problems in the first-order predicate calculus*, J. Comp. System Sciences**29**, 8–35.MathSciNetCrossRefMATHGoogle Scholar - 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.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.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.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.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.Przymusinski, T. C. [1988b],
*On constructive negation in logic programming*, Technical Report Draft, University of Texas at El Paso.Google Scholar - 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.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.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.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.Reynolds, M. [1987],
*The expressive power of query languages based on logic programming*, Ph.D. Thesis, University London.Google Scholar - 85.Reynolds, M. [1987a],
*A completeness result for logic programming*, Manuscript.Google Scholar - 86.Reynolds, M. [1988],
*Declarative meaning for logic programs with negation as failure*, Manuscript.Google Scholar - 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.Ross, K. and Topor. R. W. [1987],
*Inferring negative information from disjunctive databases*, Technical Report 87/1, University of Melbourne.Google Scholar - 89.Sakai, K. and Miyachi, T. [1983],
*Incorporating naive negation into*PROLOG, ICOT Technical Report: TR-028.Google Scholar - 90.Sato, T. [1982],
*Negation and semantics of*PROLOG*programs*, Proc. 1st International Conference on Logic Programming, 169–174.Google Scholar - 91.Sato, T. [1987],
*On the consistency of first order logic programs*, Tech. Report 87–12, Electrotechnical Laboratory, Ibarki, Japan.Google Scholar - 92.Sato, T. [1988],
*Completed logic programs and their consistency*, Typescript, Electrotechnical Laboratory, Ibaraki, Japan. To appear in J. Logic Programming.Google Scholar - 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.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.Shepherdson, J. C. [1985],
*Negation as failure*II, J. Logic Programming**3**, 185–202.MathSciNetCrossRefGoogle Scholar - 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.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.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.Shepherdson, J. C. [1989],
*Unsolvable problems for*SLDNF-*resolution*, J. Logic Programming**10**, 19–22.MathSciNetCrossRefGoogle Scholar - 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.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.Solovay, R. M. [1976],
*Provability interpretation of modal logic*, Israel Journal of Mathematics**25**, 287–304.MathSciNetCrossRefMATHGoogle Scholar - 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.Terracini, L. [1988],
*Modal interpretation for negation by failure*, Atti delPAcademia delle Scienze di Torino**122**, 81–88.MathSciNetMATHGoogle Scholar - 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.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.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.Voda, P. J. [1986],
*Choices in, and limitations of, logic programming*, Proc. 3rd Int. Conf. Logic Programming, Springer, 615–623.Google Scholar - 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