Proving Properties of Constraint Logic Programs by Eliminating Existential Variables | SpringerLink
Skip to main content
Springer Nature Link
Log in

Proving Properties of Constraint Logic Programs by Eliminating Existential Variables

  • Conference paper
Logic Programming (ICLP 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4079))

Included in the following conference series:

  • 498 Accesses

Abstract

We propose a method for proving first order properties of constraint logic programs which manipulate finite lists of real numbers. Constraints are linear equations and inequations over reals. Our method consists in converting any given first order formula into a stratified constraint logic program and then applying a suitable unfold/fold transformation strategy that preserves the perfect model. Our strategy is based on the elimination of existential variables, that is, variables which occur in the body of a clause and not in its head. Since, in general, the first order properties of the class of programs we consider are undecidable, our strategy is necessarily incomplete. However, experiments show that it is powerful enough to prove several non-trivial program properties.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Apt, K.R.: Principles of Constraint Programming. Cambridge University Press, Cambridge (2003)

    Book  MATH  Google Scholar 

  2. Apt, K.R., Bol, R.N.: Logic programming and negation: A survey. Journal of Logic Programming 19(20), 9–71 (1994)

    Article  MathSciNet  Google Scholar 

  3. Bundy, A.: The automation of proof by mathematical induction. In: Handbook of Automated Reasoning, vol. I, pp. 845–911. North-Holland, Amsterdam (2001)

    Chapter  Google Scholar 

  4. Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  5. Courcelle, B.: Equivalences and transformations of regular systems – applications to recursive program schemes and grammars. Theor. Comp. Sci. 42, 1–122 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  6. Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theoretical Computer Science 166, 101–146 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  7. Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. In: Proceedings VCL 2001, Florence, Italy, pp. 85–96. University of Southampton, UK (2001)

    Google Scholar 

  8. Fioravanti, F., Pettorossi, A., Proietti, M.: Transformation Rules for Locally Stratified Constraint Logic Programs. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 291–339. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Kott, L.: The McCarthy’s induction principle: ‘oldy’ but ‘goody’. Calcolo 19(1), 59–69 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  10. Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialization. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 63–82. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  11. Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987)

    MATH  Google Scholar 

  12. Maher, M.J.: A transformation system for deductive database modules with perfect model semantics. Theoretical Computer Science 110, 377–403 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  13. The MAP System, http://www.iasi.cnr.it/~proietti/system.html

  14. Pettorossi, A., Proietti, M.: Synthesis and transformation of logic programs using unfold/fold proofs. Journal of Logic Programming 41(2&3), 197–230 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  15. Pettorossi, A., Proietti, M.: Perfect Model Checking via Unfold/Fold Transformations. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 613–628. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Proietti, M., Pettorossi, A.: Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theor.Comp.Sci. 142(1), 89–124 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  17. Przymusinski, T.C.: On the declarative semantics of stratified deductive databases and logic programs. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 193–216. Morgan Kaufmann, San Francisco (1987)

    Google Scholar 

  18. Rabin, M.O.: Decidable theories. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 595–629. North-Holland, Amsterdam (1977)

    Chapter  Google Scholar 

  19. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of Parameterized Systems Using Logic Program Transformations. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785, pp. 172–187. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  20. Tamaki, H., Sato, T.: Unfold/fold transformation of logic programs. In: Tärnlund, S.-Å. (eds.) Proceedings of ICLP 1984, pp. 127–138, Uppsala, Sweden (1984)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISP, University of Roma Tor Vergata, Via del Politecnico 1, I-00133, Roma, Italy

    Alberto Pettorossi & Valerio Senni

  2. IASI-CNR, Viale Manzoni 30, I-00185, Roma, Italy

    Maurizio Proietti

Authors
  1. Alberto Pettorossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maurizio Proietti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Valerio Senni
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Twente, The Netherlands

    Sandro Etalle

  2. Department of Computer Science, University of Kentucky, 40506, Lexington, KY, USA

    Mirosław Truszczyński

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pettorossi, A., Proietti, M., Senni, V. (2006). Proving Properties of Constraint Logic Programs by Eliminating Existential Variables. In: Etalle, S., Truszczyński, M. (eds) Logic Programming. ICLP 2006. Lecture Notes in Computer Science, vol 4079. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11799573_15

Download citation

  • DOI: https://doi.org/10.1007/11799573_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36635-5

  • Online ISBN: 978-3-540-36636-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics