×

Constraint-based correctness proofs for logic program transformations. (English) Zbl 1259.68036


MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N17 Logic programming
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Apt KR (1990) Introduction to logic programming. In: van Leeuwen J (ed.) Handbook of theoretical computer science. Elsevier, Amsterdam, pp 493–576
[2] Bossi A, Cocco N (1994) Preserving universal termination through unfold/fold. In: Proceedings ALP ’94, Lecture notes in computer science, vol 850. Springer, Berlin, pp 269–286 · Zbl 0988.68513
[3] Bossi A, Cocco N, Etalle S (1992) On safe folding. In: Proceedings PLILP ’92, Leuven, Belgium, Lecture notes in computer science, vol 631. Springer, Berlin, pp 172–186
[4] Burstall RM, Darlington J (1977) A transformation system for developing recursive programs. J ACM 24(1): 44–67 · Zbl 0343.68014 · doi:10.1145/321992.321996
[5] Bezem M (1989) Characterizing termination of logic programs with level mappings. In: Lusk EL, Overbeek RA (eds) Proceedings of the North American Conference on Logic Programming, Cleveland, Ohio, USA. MIT Press, Cambridge, pp 69–80
[6] Cook J, Gallagher JP (1994) A transformation system for definite programs based on termination analysis. In: Fribourg L, Turini F (eds.) Proceedings of LOPSTR ’94 and META’94, Pisa, Italy, Lecture notes in computer science, vol 883. Springer, Berlin, pp 51–68
[7] Dershowitz N (1987) Termination of rewriting. J Symb Comput 3(1–2): 69–116 · Zbl 0637.68035 · doi:10.1016/S0747-7171(87)80022-6
[8] Dix J (1995) A classification theory of semantics of normal logic programs: II weak properties. Fundam Inform XXII(3): 257–288 · Zbl 0829.68022
[9] Etalle S, Gabbrielli M (1996) Transformations of CLP modules. Theor Comput Sci 166: 101–146 · Zbl 0872.68021 · doi:10.1016/0304-3975(95)00148-4
[10] Fuhs C, Giesl J, Middeldorp A, Schneider-Kamp P, Thiemann R, Zankl H (2007) SAT solving for termination analysis with polynomial interpretations. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT ’07, Lisbon, Portugal, May 28–31, 2007. Lecture notes in computer science, vol 4501. Springer, Berlin, pp 340–354 · Zbl 1214.68352
[11] Gergatsoulis M, Katzouraki M (1994) Unfold/fold transformations for definite clause programs. In: Hermenegildo M, Penjam J (eds) Proceedings sixth International Symposium on Programming Language Implementation and Logic Programming, PLILP ’94. Lecture notes in computer science, vol 844. Springer, Berlin, pp 340–354
[12] Jaffar J, Maher M (1994) Constraint logic programming: a survey. J Logic Program 19/20: 503–581 · Zbl 00639141 · doi:10.1016/0743-1066(94)90033-7
[13] Kanamori T, Fujita H (1986) Unfold/fold transformation of logic programs with counters. Technical Report 179, ICOT, Tokyo, Japan · Zbl 0642.68023
[14] Kott L (1978) About transformation system: a theoretical study. In: 3ème Colloque International sur la Programmation, Paris (France). Dunod, Paris, pp 232–247
[15] Kott L (1982) The McCarthy’s induction principle: ’oldy’ but ’goody’. Calcolo 19(1): 59–69 · Zbl 0526.68014 · doi:10.1007/BF02576192
[16] Lankford DS (1979) On proving term rewriting systems are noetherian. MTP 3, Lousiana Technical University
[17] Lloyd JW (1987) Foundations of logic programming, 2nd edn. Springer, Berlin · Zbl 0668.68004
[18] Lau K-K, Ornaghi M, Pettorossi A, Proietti M (1995) Correctness of logic program transformation based on existential termination. In: Lloyd JW (ed.) Proceedings of the 1995 International Logic Programming Symposium, ILPS ’95. MIT Press, Cambridge, pp 480–494
[19] Maher MJ (1987) Correctness of a logic program transformation system. IBM Research Report RC 13496, T. J. Watson Research Center
[20] Maher MJ (1993) A transformation system for deductive database modules with perfect model semantics. Theor Comput Sci 110: 377–403 · Zbl 0780.68022 · doi:10.1016/0304-3975(93)90013-J
[21] MAP transformation system (2011). http://www.iasi.cnr.it/\(\sim\)proietti/system.html
[22] McCarthy J (1963) Towards a mathematical science of computation. In: Popplewell CM (ed.) Information processing: Proceedings of IFIP, vol 1962. North Holland, Amsterdam, pp 21–28
[23] Nguyen MT, De Schreye D, Giesl J, Schneider-Kamp P (2011) Polytool: polynomial interpretations as a basis for termination analysis of logic programs. Theory Pract Logic Program 11(1): 33–63 · Zbl 1222.68064 · doi:10.1017/S1471068410000025
[24] Pettorossi A, Proietti M (1999) Synthesis and transformation of logic programs using unfold/fold proofs. J Logic Program 41(2–3): 197–230 · Zbl 0944.68024 · doi:10.1016/S0743-1066(99)00029-1
[25] Pettorossi A, Proietti M (2008) Totally correct logic program transformations via well-founded annotations. High Order Symb Comput 21: 193–234 · Zbl 1194.68095 · doi:10.1007/s10990-008-9024-6
[26] Pettorossi A, Proietti M, Senni V (2007) Automatic correctness proofs for logic program transformations. In: Dahl V, Niemelä I (eds.) Proceedings of the 23rd International Conference on Logic Programming, ICLP ’07. Lecture notes in computer science, vol 4670. Springer, pp 364–379 · Zbl 1213.68207
[27] Pettorossi A, Proietti M, Senni V (2010) Transformations of logic programs on infinite lists. Theory Practice Logic Program 10(4–6):383–399 (Special Issue on the 26th International Conference on Logic Programming, ICLP ’10, Edinburgh, Scotland, UK) · Zbl 1209.68096
[28] Roychoudhury A, Narayan Kumar K, Ramakrishnan CR, Ramakrishnan IV (2002) Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. Int J Found Comput Sci 13(3):387–403 · Zbl 1066.68016
[29] Roychoudhury A, Narayan Kumar K, Ramakrishnan CR, Ramakrishnan IV (2004) An unfold/fold transformation framework for definite logic programs. ACM Trans Program Lang Syst 26:264–509 · Zbl 0953.68031
[30] Sands D (1996) Total correctness by local improvement in the transformation of functional programs. ACM Toplas 18(2): 175–234 · Zbl 01936338 · doi:10.1145/227699.227716
[31] Seki H (1991) Unfold/fold transformation of stratified programs. Theor Comput Sci 86: 107–139 · Zbl 0737.68016 · doi:10.1016/0304-3975(91)90007-O
[32] Seki H (2009) On negative unfolding in the answer set semantics. In: Hanus M (ed) Logic-based Program Synthesis and Transformation, 18th International Symposium, LOPSTR ’08, Valencia, Spain, July 17–18, 2008, Revised Selected Papers. Lecture notes in computer science, vol 5438. Springer, Berlin, pp 168–184
[33] Seki H (2010) On inductive and coinductive proofs via unfold/fold transformations. In: De Schreye D (ed) Proceedings of the 19th International Symposium on Logic-based Program Synthesis and Transformation, LOPSTR ’09, Coimbra, Portugal, September 9–11, 2009. Lecture notes in computer science, vol 6037. Springer, Berlin, pp 82–96 · Zbl 1284.68201
[34] Seki H (2011) Proving properties of co-logic programs by unfold/fold transformations. In: Vidal G (ed) Preliminary Proceedings of the 21th International Symposium on Logic-based Synthesis and Transformation, LOPSTR ’11, July 18–20, 2011, Odense, Denmark. University of Southern Denmark, pp 112–126
[35] Simon L, Mallya A, Bansal A, Gupta G (2006) Coinductive logic programming. In: Etalle S, Truszczyński M (eds) Proceedings of the 22nd International Conference on Logic Programming, ICLP ’06, Seattle, WA, USA, August 17–20, 2006. Lecture notes in computer science, vol 4079. Springer, Berlin, pp 330–345 · Zbl 1131.68400
[36] Sato T, Tamaki H (1985) Examples of logic program transformation and synthesis. Case studies of transformation and synthesis of logic programs done up to February’85. Unpublished manuscript, Ibaraki University, Japan
[37] Tamaki H, Sato T (1984) Unfold/fold transformation of logic programs. In: Tärnlund S-Å (ed) Proceedings of the Second International Conference on Logic Programming, ICLP ’84, Uppsala, Sweden, 1984. Uppsala University, pp 127–138
[38] Tamaki H, Sato T (1986) A generalized correctness proof of the unfold/fold logic program transformation. Technical Report 86-4, Ibaraki University, Japan
[39] Wand M (1980) Continuation-based program transformation strategies. J ACM 27(1): 164–180 · Zbl 0429.68028 · doi:10.1145/322169.322183
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.