SpringerLink
Log in

Proof-Theoretic Foundations of Normal Logic Programs

  • Chapter
  • First Online:
Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems

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

  • 189 Accesses

Abstract

There are several semantics in logic programming for negation as failure. These semantics can be realized with a combination of induction and coinduction, and this realization can be used to develop a goal-directed method of computing models. In essence, the difference between these semantics is how they resolve the unstratified portions of a program. In this paper, restricting ourselves to the propositional case, we show how the semantics of normal logic programs is a mixture of induction and coinduction, and how we can use coinduction to resolve the cycles (or loops) formed by the rules in a program. We present denotational semantics based on a fixed point of a function and show its equivalence to the use of induction and coinduction. We take a look at the different ways a semantics may resolve cycles, and show how to implement two popular semantics, well-founded and stable models, as well as co-stable model semantics. Finally, we present operational semantics as a parametrized goal-directed execution algorithm that allows us to determine how cycles are resolved.

Dedicated to Professor Manuel Hermenegildo on the occasion of his 60th birthday. Authors are grateful for support from US NSF and US DoD.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 109.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 139.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Aczel, P.: Non-well-founded sets, CSLI lecture notes series, vol. 14. CSLI (1988)

    Google Scholar 

  2. Apt, K.R., Bol, R.N.: Logic programming and negation: a survey. J. Log. Program. 19(20), 9–71 (1994). https://doi.org/10.1016/0743-1066(94)90024-8

  3. Arias, J., Carro, M., Salazar, E., Marple, K., Gupta, G.: Constraint answer set programming without grounding. TPLP 18(3–4), 337–354 (2018)

    MathSciNet  MATH  Google Scholar 

  4. Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  5. Basu, K., Shakerin, F., Gupta, G.: AQuA: ASP-based visual question answering. In: Komendantskaya, E., Liu, Y.A. (eds.) PADL 2020. LNCS, vol. 12007, pp. 57–72. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-39197-3_4

    Chapter  Google Scholar 

  6. Chen, Z., Marple, K., Salazar, E., Gupta, G., Tamil, L.: A physician advisory system for chronic heart failure management based on knowledge patterns. Theory Pract. Log. Program. 16(5–6), 604–618 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  7. Clark, K.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Springer, Boston, MA (1978). https://doi.org/10.1007/978-1-4684-3384-5_11

  8. Dix, J.: A classification theory of semantics of normal logic programs: I. strong properties. Fundam. Inform. 22(3), 227–255 (1995)

    Google Scholar 

  9. Dix, J.: A classification theory of semantics of normal logic programs: II. weak properties. Fundam. Inform. 22(3), 257–288 (1995)

    Google Scholar 

  10. Fitting, M., Ben-Jacob, M.: Stratified and three-valued logic programming semantics. In: Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, 15–19 August 1988 (2 Volumes), pp. 1054–1069 (1988)

    Google Scholar 

  11. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, 15–19 August 1988 (2 Volumes), pp. 1070–1080 (1988)

    Google Scholar 

  12. Gupta, G., Marple, K., Others: Coinductive answer set programming or consistency-based computing (2012). Co-LP 2012 - A workshop on Coinductive Logic Programming, https://utdallas.edu/~gupta/coasp.pdf

  13. Gupta, G., Saeedloei, N., DeVries, B., Min, R., Marple, K., Kluźniak, F.: Infinite computation, co-induction and computational logic. In: Proceedings of the Coalgebra and Algebra in Computer Science (CALCO), pp. 40–54 (2011)

    Google Scholar 

  14. Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. EATCS Bull. 62, 62–222 (1997)

    MATH  Google Scholar 

  15. Klemen, M., Stulova, N., López-García, P., Morales, J.F., Hermenegildo, M.V.: Static performance guarantees for programs with runtime checks. In: Sabel, D., Thiemann, P. (eds.) Proceedings of the PPDP, pp. 13:1–13:13. ACM (2018)

    Google Scholar 

  16. Leinster, T.: Basic Category Theory. Cambridge University Press, Cambridge (2016)

    Google Scholar 

  17. Liu, Y.A., Stoller, S.D.: Founded semantics and constraint semantics of logic rules. J. Log. Comput. 30(8), 1609–1668 (2020)

    Article  MathSciNet  MATH  Google Scholar 

  18. Lloyd, J.W.: Foundations of Logic Programming. Springer, Berlin, Heidelberg (1987). https://doi.org/10.1007/978-3-642-83189-8

  19. Marple, K., Bansal, A., Min, R., Gupta, G.: Goal-directed execution of answer set programs. In: Principles and Practice of Declarative Programming, PPDP 2012, Leuven, Belgium - 19–21 September 2012, pp. 35–44 (2012)

    Google Scholar 

  20. Marple, K., Gupta, G.: Galliwasp: a goal-directed answer set solver. In: Logic-Based Program Synthesis and Transformation, 22nd International Symposium, LOPSTR 2012, Leuven, Belgium, 18–20 September 2012, Revised Selected Papers, pp. 122–136 (2012)

    Google Scholar 

  21. Marple, K., Salazar, E., Gupta, G.: Computing stable models of normal logic programs without grounding (2017). ar**v preprint ar**v:1709.00501

  22. Min, R.K.: Predicate Answer Set Programming with Coinduction. Ph.D. thesis, University of Texas at Dallas, Richardson, TX, USA (2009)

    Google Scholar 

  23. Minker, J. (ed.): Foundations of Deductive Databases and Logic Programming. Morgan Kaufmann Publishers Inc., Burlington (1988)

    Google Scholar 

  24. Roşu, G., Lucanu, D.: Circular coinduction: a proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 127–144. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03741-2_10

    Chapter  Google Scholar 

  25. Salazar, E.E.: NAF-Based Logic Semantics: Proof-Theoretic Generalization and Non-Ground Extension. Ph.D. thesis, Dept of Computer Science, UT Dallas (2019)

    Google Scholar 

  26. Salazar, E.E., Gupta, G.: Proof-theoretic foundations of normal logic programs, Technical report, dept of comp. sci., UT Dallas (2017). https://utdallas.edu/~gupta/prooftheoretic.pdf

  27. Seki, H.: On dual programs in co-logic programming. In: Falaschi, M. (ed.) LOPSTR 2015. LNCS, vol. 9527, pp. 21–35. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27436-2_2

    Chapter  MATH  Google Scholar 

  28. Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: extending logic programming with coinduction. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 472–483. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73420-8_42

    Chapter  MATH  Google Scholar 

  29. Van Gelder, A., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general logic programs. J. Assoc. Comput. Mach. 38(03), 620–650 (1991)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Texas at Dallas, Richardson, USA

    Elmer Salazar & Gopal Gupta

Authors
  1. Elmer Salazar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gopal Gupta
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gopal Gupta .

Editor information

Editors and Affiliations

  1. IMDEA Software Institute, Pozuelo de Alarcón, Madrid, Spain

    Pedro Lopez-Garcia

  2. Roskilde University, Roskilde, Denmark

    John P. Gallagher

  3. Università di Verona, Verona, Italy

    Roberto Giacobazzi

Rights and permissions

Reprints and permissions

Copyright information

© 2023 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Salazar, E., Gupta, G. (2023). Proof-Theoretic Foundations of Normal Logic Programs. In: Lopez-Garcia, P., Gallagher, J.P., Giacobazzi, R. (eds) Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems. Lecture Notes in Computer Science, vol 13160. Springer, Cham. https://doi.org/10.1007/978-3-031-31476-6_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-31476-6_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-31475-9

  • Online ISBN: 978-3-031-31476-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation