Skip to main content
SpringerLink
Log in

On Inductive and Coinductive Proofs via Unfold/Fold Transformations

  • Conference paper
Logic-Based Program Synthesis and Transformation (LOPSTR 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6037))

Abstract

We consider a new application condition of negative unfolding, which guarantees its safe use in unfold/fold transformation of stratified logic programs. The new condition of negative unfolding is a natural one, since it is considered as a special case of replacement rule. The correctness of our unfold/fold transformation system in the sense of the perfect model semantics is proved. We then consider the coinductive proof rules proposed by Jaffar et al. We show that our unfold/fold transformation system, when used together with Lloyd-Topor transformation, can prove a proof problem which is provable by the coinductive proof rules by Jaffar et al. To this end, we propose a new replacement rule, called sound replacement, which is not necessarily equivalence-preserving, but is essential to perform a reasoning step corresponding to coinduction.

This work was partially supported by JSPS Grant-in-Aid for Scientific Research (C) 21500136.

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

Access this chapter

Log in via an institution
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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

  2. Aravindan, C., Dung, P.M.: On the Correctness of Unfold/fold Transformation of Normal and Extended Logic Programs. J. of Logic Programming 24(3), 295–322 (1995)

    Article  MathSciNet  Google Scholar 

  3. 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)

    Google Scholar 

  4. Jaffar, J., Santosa, A., Voicu, R.: A Coinduction Rule for Entailment of Recursively Defined Properties. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 493–508. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Kanamori, T., Horiuchi, K.: Construction of Logic Programs Based on Generalized Unfold/Fold Rules. In: Proc. the 4th Intl. Conf. on Logic Programming, pp. 744–768 (1987)

    Google Scholar 

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

    MATH  Google Scholar 

  7. Pettorossi, A., Proietti, M.: Transformation of Logic Programs: Foundations and Techniques. J. of Logic Programming 19/20, 261–320 (1994)

    Article  MathSciNet  Google Scholar 

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

  9. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: Beyond Tamaki-Sato Style Unfold/fold Transformations for Normal Logic Programs. Int. Journal on Foundations of Computer Science 13(3), 387–403 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  10. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: An Unfold/fold Transformation Framework for Definite Logic Programs. ACM Trans. on Programming Languages and Systems 26(3), 464–509 (2004)

    Article  Google Scholar 

  11. Seki, H.: On Negative Unfolding in the Answer Set Semantics. In: Hanus, M. (ed.) LOPSTR 2008. LNCS, vol. 5438, pp. 168–184. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Tamaki, H., Sato, T.: Unfold/Fold Transformation of Logic Programs. In: Proc. 2nd Int. Conf. on Logic Programming, pp. 127–138 (1984)

    Google Scholar 

  13. Tamaki, H., Sato, T.: A Generalized Correctness Proof of the Unfold/Fold Logic Program Transformation, Technical Report, No. 86-4, Ibaraki Univ., Japan (1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, Nagoya Inst. of Technology, Showa-ku, Nagoya, 466-8555, Japan

    Hirohisa Seki

Authors
  1. Hirohisa Seki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, K.U.Leuven, Celestijnenlaan 200A, B-3001, Heverlee, Belgium

    Danny De Schreye

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Seki, H. (2010). On Inductive and Coinductive Proofs via Unfold/Fold Transformations. In: De Schreye, D. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2009. Lecture Notes in Computer Science, vol 6037. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12592-8_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-12592-8_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-12591-1

  • Online ISBN: 978-3-642-12592-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation