Abstract
We present a framework for unfold/fold transformation of co-logic programs, where each predicate is annotated as either inductive or coinductive, and the declarative semantics of co-logic programs is defined by an alternating fixpoint model: the least fixpoints for inductive predicates and the greatest fixpoints for coinductive predicates. We show that straightforward applications of conventional program transformation rules are not adequate for co-logic programs, and propose new conditions which ensure the preservation of the intended semantics of co-logic programs through program transformation. We then examine the use of our transformation rules for proving properties of co-logic programs which specify computations over infinite structures. We show by some examples in the literature that our method based on unfold/fold transformation can be used for verifying some properties of Büchi automata and nested automata.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Burstall, R.M., Darlington, J.: A Transformation System for Developing Recursive Programs. J. ACM 24(1), 44–67 (1977)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Colmerauer, A.: Prolog and Infinite Trees. In: Logic Programming, pp. 231–251. Academic Press (1982)
Colmerauer, A.: Equations and Inequations in Finite and Infinite Trees. In: Proc. FGCS 1984, Tokyo, pp. 85–99 (1984)
Etalle, S., Gabbrielli, M.: Transformations of CLP Modules. Theor. Comput. Sci., 101–146 (1996)
Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive Logic Programming and Its Applications. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 27–44. Springer, Heidelberg (2007)
Jaffar, J., Lassez, J.-L., Maher, M. J.: A theory of complete logic programs with equality. The Journal of Logic Programming 1(3), 211–223 (1984)
Jaffar, J., Stuckey, P.: Semantics of infinite tree logic programming. Theoretical Computer Science 46, 141–158 (1986)
Jaffar, J., Maher, M.J.: Constraint Logic Programming: A Survey. J. Log. Program. 19/20, 503–581 (1994)
Kott, L.: Unfold/fold program transformations. In: Nivat, M., Reynolds, J.C. (eds.) Algebraic Methods in Semantics, ch. 12, pp. 411–434. Cambridge University Press (1985)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer (1987)
Min, R., Gupta, G.: Coinductive Logic Programming with Negation. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 97–112. Springer, Heidelberg (2010)
Pettorossi, A., Proietti, M.: Transformation of Logic Programs: Foundations and Techniques. J. Logic Programming 19/20, 261–320 (1994)
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., Senni, V.: Deciding Full Branching Time Logic by Program Transformation. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 5–21. Springer, Heidelberg (2010)
Pettorossi, A., Proietti, M., Senni, V.: Transformations of logic programs on infinite lists. Theory and Practice of Logic Programming 10, 383–399 (2010)
Przymusinski, T.C.: On the Declarative and Procedural Semantics of Logic Programs. J. Automated Reasoning 5(2), 167–205 (1989)
Seki, H.: On Inductive and Coinductive Proofs via Unfold/Fold Transformations. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 82–96. Springer, Heidelberg (2010)
Seki, H.: Unfold/Fold Transformation of Stratified Programs. Theoretical Computer Science 86, 107–139 (1991)
Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive Logic Programming. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 330–345. Springer, Heidelberg (2006)
Simon, L.E.: Extending Logic Programming with Coinduction, Ph.D. Dissertation, University of Texas at Dallas (2006)
Tamaki, H., Sato, T.: Unfold/Fold Transformation of Logic Programs. In: Proc. 2nd Int. Conf. on Logic Programming, pp. 127–138 (1984)
Tamaki, H., Sato, T.: A Generalized Correctness Proof of the Unfold/Fold Logic Program Transformation, Technical Report, No. 86-4, Ibaraki Univ. (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seki, H. (2012). Proving Properties of Co-Logic Programs by Unfold/Fold Transformations. In: Vidal, G. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2011. Lecture Notes in Computer Science, vol 7225. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32211-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-32211-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32210-5
Online ISBN: 978-3-642-32211-2
eBook Packages: Computer ScienceComputer Science (R0)