Skip to main content
SpringerLink
Log in

Logic Programming and Co-inductive Definitions

  • Conference paper
  • First Online:
Computer Science Logic (CSL 2000)

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

Included in the following conference series:

Abstract

This paper aims to define a complete semantics for a class of non-terminating logic programs. Standard approaches to deal with this problem consist in concentrating on programs where infinite derivations can be seen as computing, in the limit, some ”infinite object”. This is usually done by extending the domain of computation with infinite elements and then defining the meaning of programs in terms of greatest fixpoints. The main drawback of these approaches is that the semantics defined is not complete. The approach considered here is exactly the opposite. We concentrate on the infinite derivations that do not compute an infinite term: this paper studies the operational counterpart of the greatest fixpoint of the one-step-inference operator for the \( \mathcal{C} \)-semantics. The main result is that such fixpoint corresponds to the set of atoms that have a non-failing fair derivation with the additional property that complete information over a variable is obtained after finitely many steps.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M.A. Nait Abdallah. On the interpretation of infinite computations in logic programming. In J. Paredaens, editor, 11th International Colloquium on Automata, Languages and Programming, ICALP’84, volume 172 of LNCS, pages 358–370. Springer-Verlag, 1984.

    Google Scholar 

  2. P. Aczel. An introduction to inductive definitions. In K.J. Barwise, editor, Handbook of Mathematical Logic, Studies in Logic and Foundations of Mathematics. North Holland, 1977.

    Google Scholar 

  3. T. Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, 1st International Workshop on Types for Proofs and Programs, TYPES’93, volume 806 of LNCS, pages 62–78. Springer-Verlag, 1994.

    Google Scholar 

  4. F.S. de Boer, A. Di Pierro, and C. Palamidessi. Nondeterminism and infinite computations in constraint programming. Theoretical Computer Science, 151(1):37–78, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  5. P. Deransart and J. Maluszynski. A Grammatical View of Logic Programming. The MIT Press, 1993.

    Google Scholar 

  6. M. Falaschi, G. Levi, C. Palamidessi, and M. Martelli. Declarative modelingof the operational behavior of logic languages. Theoretical Computer Science, 69(3):289–318, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  7. W.G. Golson. Toward a declarative semantics for infinite objects in logic programming. Journal of Logic Programming, 5(2):151–164, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  8. J. Hein. Completions of perpetual logic programs. Theoretical Computer Science, 99(1):65–78, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  9. G. Huet. A Uniform Approach to Type Theory, volume Logical Foundations of Functional Programming, pages 337–398. Addison-Wesley, 1990.

    Google Scholar 

  10. J. Ja.ar and J.L. Lassez. Constraint Logic Programming. Technical Report 86/74, Monash University, Victoria, Australia, June 1986.

    Google Scholar 

  11. J. Ja.ar and P.J. Stuckey. Semantics of infinite tree logic programming. Theoretical Computer Science, 46(2–3):141–158, 1986.

    MathSciNet  Google Scholar 

  12. M. Jaume. Logic programming and co-inductive definitions. Research Report 98–140, Enpc-Cermics, 1998.

    Google Scholar 

  13. M. Jaume. A full formalisation of SLD-resolution in the calculus of inductive constructions. Journal of Automated Reasoning, 23(3-4):347–371, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  14. R. Lalement. Computation as Logic. Prentice Hall International Series in Computer Science, 1993.

    Google Scholar 

  15. G. Levi and C. Palamidessi. Contributions to the semantics of logic perpetual processes. Acta Informatica, 25(6):691–711, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  16. J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.

    Google Scholar 

  17. L.C. Paulson and A.W. Smith. Logic programming, functional programming, and inductive definitions. In P. Schroeder-Heister, editor, International Workshop on Extensions of Logic Programming, volume 475 of LNCS, pages 283–310. Springer-Verlag, 1989.

    Chapter  Google Scholar 

  18. A. Podelski, W. Charatonik, and M. Müller. Set-based failure analysis for logic programs and concurrent constraint programs. In S. Doaitse Swierstra, editor, 8th European Symposium on Programming, ESOP’99, LNCS, pages 177–192. Springer-Verlag, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cermics-École Nationale des Ponts et Chaussées, Champs sur Marne, 77455, Marne-La-Vallee Cedex 2, France

    Mathieu Jaume

Authors
  1. Mathieu Jaume
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Department of Biology, Boston College, Fulton Hall 410B, Chestnut Hill, MA, 02467, USA

    Peter G. Clote

  2. Mathematisches Institut, Ludwig-Maximilian-Universität München, Theresienstr. 39, 80333, München, Germany

    Helmut Schwichtenberg

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jaume, M. (2000). Logic Programming and Co-inductive Definitions. In: Clote, P.G., Schwichtenberg, H. (eds) Computer Science Logic. CSL 2000. Lecture Notes in Computer Science, vol 1862. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44622-2_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-44622-2_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67895-3

  • Online ISBN: 978-3-540-44622-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation