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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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)
Apt, K.R.: Introduction to logic programming. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 493–576. Elsevier, Amsterdam (1990)
Apt, K.R.: From Logic Programming to Prolog. Prentice Hall, London (1997)
Apt, K.R., Bol, R.N.: Logic programming and negation: A survey. Journal of Logic Programming 19-20, 9–71 (1994)
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)
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)
Bensaou, N., Guessarian, I.: Transforming constraint logic programs. Theoretical Computer Science 206, 81–125 (1998)
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)
Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)
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)
Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theoretical Computer Science 166, 101–146 (1996)
Fioravanti, F.: Transformation of Constraint Logic Programs for Software Specialization and Verification. PhD thesis, Università di Roma “La Sapienza”, Italy (2002)
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)
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)
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)
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)
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)
Hogger, C.J.: Derivation of logic programs. Journal of the ACM 28(2), 372–392 (1981)
Jaffar, J., Maher, M.: Constraint logic programming: A survey. Journal of Logic Programming 19-20, 503–581 (1994)
Jaffar, J., Maher, M., Marriott, K., Stuckey, P.: The semantics of constraint logic programming. Journal of Logic Programming 37, 1–46 (1998)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)
Kanamori, T., Fujita, H.: Unfold/fold transformation of logic programs with counters. Technical Report 179, ICOT, Tokyo, Japan (1986)
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)
Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming 2(4&5), 461–515 (2002)
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)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)
Maher, M.J.: A transformation system for deductive database modules with perfect model semantics. Theoretical Computer Science 110, 377–403 (1993)
Marriott, K., Stuckey, P.: Programming with Constraints: An Introduction. MIT Press, Cambridge (1998)
Pettorossi, A., Proietti, M.: Transformation of logic programs: Foundations and techniques. Journal of Logic Programming 20, 261–320 (1994)
Pettorossi, A., Proietti, M.: Synthesis and transformation of logic programs using unfold/fold proofs. Journal of Logic Programming 41(2&3), 197–230 (1999)
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)
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)
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)
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)
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)
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)
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)
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)
Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM Toplas 18(2), 175–234 (1996)
Sato, T.: An equivalence preserving first order unfold/fold transformation system. Theoretical Computer Science 105, 57–84 (1992)
Sato, T., Tamaki, H.: Transformational logic program synthesis. In: Proceedings of the International Conference on Fifth Generation Computer Systems, pp. 195–201. ICOT (1984)
Seki, H.: Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107–139 (1991)
Seki, H.: Unfold/fold transformation of general logic programs for well-founded semantics. Journal of Logic Programming 16(1&2), 5–23 (1993)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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