Skip to main content

Transformation Rules for Locally Stratified Constraint Logic Programs

  • Chapter

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

Abstract

We propose a set of transformation rules for constraint logic programs with negation. We assume that every program is locally stratified and, thus, it has a unique perfect model. We give sufficient conditions which ensure that the proposed set of transformation rules preserves the perfect model of the programs. Our rules extend in some respects the rules for logic programs and constraint logic programs already considered in the literature and, in particular, they include a rule for unfolding a clause with respect to a negative literal.

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

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alpuente, M., Falaschi, M., Moreno, G., Vidal, G.: A transformation system for lazy functional logic programs. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 147–162. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  2. Apt, K.R.: Introduction to logic programming. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 493–576. Elsevier, Amsterdam (1990)

    Google Scholar 

  3. Apt, K.R.: From Logic Programming to Prolog. Prentice Hall, London (1997)

    Google Scholar 

  4. 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 

  5. Autebert, J.-M., Berstel, J., Boasson, L.: Context-free languages and pushdown automata. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 111–174. Springer, Berlin (1997)

    Google Scholar 

  6. Basin, D., Deville, Y., Flener, P., Hamfelt, A., Nilsson, J.F.: Synthesis of programs in computational logic. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 30–65. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Bensaou, N., Guessarian, I.: Transforming constraint logic programs. Theoretical Computer Science 206, 81–125 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  8. Bossi, A., Cocco, N., Etalle, S.: Transforming normal programs by replacement. In: Pettorossi, A. (ed.) META 1992. LNCS, vol. 649, pp. 265–279. Springer, Heidelberg (1992)

    Google Scholar 

  9. 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 

  10. Garcia de la Banda, M., Hermenegildo, M., Bruynooghe, M., Dumortier, V., Janssens, G., Simoens, W.: Global analysis of constraint logic programs. ACM Transactions on Programming Languages and Systems 18(5), 564–614 (1996)

    Article  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  12. Fioravanti, F.: Transformation of Constraint Logic Programs for Software Specialization and Verification. PhD thesis, Università di Roma “La Sapienza”, Italy (2002)

    Google Scholar 

  13. Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. In: Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL 2001, Florence (Italy), Technical Report DSSE-TR-2001-3, pp. 85–96. University of Southampton, UK (2001)

    Google Scholar 

  14. Fioravanti, F., Pettorossi, A., Proietti, M.: Specialization with clause splitting for deriving deterministic constraint logic programs. In: Proceedings of the IEEE International Conference on Systems, Man and Cybernetics, Hammamet (Tunisia), IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  15. Fribourg, L., Olsén, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 96–107. Springer, Heidelberg (1997)

    Google Scholar 

  16. Gardner, P.A., Shepherdson, J.C.: Unfold/fold transformations of logic programs. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic, Essays in Honor of Alan Robinson, pp. 565–583. MIT, Cambridge (1991)

    Google Scholar 

  17. Gergatsoulis, M., Katzouraki, M.: Unfold/fold transformations for definite clause programs. In: Penjam, J. (ed.) PLILP 1994. LNCS, vol. 844, pp. 340–354. Springer, Heidelberg (1994)

    Google Scholar 

  18. Hogger, C.J.: Derivation of logic programs. Journal of the ACM 28(2), 372–392 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  19. Jaffar, J., Maher, M.: Constraint logic programming: A survey. Journal of Logic Programming 19-20, 503–581 (1994)

    Article  MathSciNet  Google Scholar 

  20. Jaffar, J., Maher, M., Marriott, K., Stuckey, P.: The semantics of constraint logic programming. Journal of Logic Programming 37, 1–46 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  21. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)

    MATH  Google Scholar 

  22. Kanamori, T., Fujita, H.: Unfold/fold transformation of logic programs with counters. Technical Report 179, ICOT, Tokyo, Japan (1986)

    Google Scholar 

  23. Kanamori, T., Horiuchi, K.: Construction of logic programs based on generalized unfold/fold rules. In: Proceedings of the Fourth International Conference on Logic Programming, pp. 744–768. The MIT Press, Cambridge (1987)

    Google Scholar 

  24. Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming 2(4&5), 461–515 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  25. 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 

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

    MATH  Google Scholar 

  27. 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 

  28. Marriott, K., Stuckey, P.: Programming with Constraints: An Introduction. MIT Press, Cambridge (1998)

    MATH  Google Scholar 

  29. Pettorossi, A., Proietti, M.: Transformation of logic programs: Foundations and techniques. Journal of Logic Programming 20, 261–320 (1994)

    Article  MathSciNet  Google Scholar 

  30. 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 

  31. 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 

  32. Pettorossi, A., Proietti, M.: Program Derivation = Rules + Strategies. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2407, pp. 273–309. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  33. Pettorossi, A., Proietti, M., Renault, S.: Reducing nondeterminism while specializing logic programs. In: Proc. 24th ACM Symposium on Principles of Programming Languages, Paris, France, pp. 414–427. ACM Press, New York (1997)

    Google Scholar 

  34. Proietti, M., Pettorossi, A.: Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science 142(1), 89–124 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  35. 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 

  36. Roychoudhury, K., Narayan Kumar, C.R., Ramakrishnan, I.V.: Verification of parameterized systems using logic program transformations. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 172–187. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  37. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. International Journal on Foundations of Computer Science 13(3), 387–403 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  38. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: A parameterized unfold/fold transformation framework for definite logic programs. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 396–413. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  39. Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM Toplas 18(2), 175–234 (1996)

    Article  MathSciNet  Google Scholar 

  40. Sato, T.: An equivalence preserving first order unfold/fold transformation system. Theoretical Computer Science 105, 57–84 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  41. Sato, T., Tamaki, H.: Transformational logic program synthesis. In: Proceedings of the International Conference on Fifth Generation Computer Systems, pp. 195–201. ICOT (1984)

    Google Scholar 

  42. Seki, H.: Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107–139 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  43. Seki, H.: Unfold/fold transformation of general logic programs for well-founded semantics. Journal of Logic Programming 16(1&2), 5–23 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  44. Tamaki, H., Sato, T.: Unfold/fold transformation of logic programs. In: Tärnlund, S.-Å. (ed.) Proceedings of the Second International Conference on Logic Programming, pp. 127–138. Uppsala University, Uppsala (1984)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Fioravanti, F., Pettorossi, A., Proietti, M. (2004). Transformation Rules for Locally Stratified Constraint Logic Programs. In: Bruynooghe, M., Lau, KK. (eds) Program Development in Computational Logic. Lecture Notes in Computer Science, vol 3049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25951-0_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-25951-0_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22152-4

  • Online ISBN: 978-3-540-25951-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics