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

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.

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