Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

On Induction Principles for Diamond-Free Partial Orders

  • Conference paper
  • First Online:
Information and Communication Technologies in Education, Research, and Industrial Applications (ICTERI 2020)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 1308))

  • 260 Accesses

Abstract

We propose a formulation of an induction principle for diamond-free partial orders, which can be considered as a generalization of one of the variants of the real induction principle. This principle may be useful for specification and verification of non-discrete systems using interactive proof assistant software. As an example, a formalization in Isabelle proof assistant is presented.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 EPUB and 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

We’re sorry, something doesn't seem to be working properly.

Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

References

  1. Clark, P.: The Instructor’s Guide to Real Induction (2012). http://arxiv.org/abs/1208.0973

  2. Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: Proceedings of LICS 2018, pp. 819–828 (2018)

    Google Scholar 

  3. Platzer, A., Tan, Y.K.: Differential Equation Invariance Axiomatization (2019). http://arxiv.org/abs/1905.13429

  4. Clark, P.: The instructor’s guide to real induction. Math. Mag. 92, 136–150 (2019)

    Article  MathSciNet  Google Scholar 

  5. Raoult, J.-C.: Proving open properties by induction. Inf. Process. Lett. 29, 19–23 (1988)

    Article  MathSciNet  Google Scholar 

  6. A principle of mathematical induction for partially ordered sets with infima. Web page: https://mathoverflow.net/questions/38238

  7. Ivanov, I.: On induction for diamond-free directed complete partial orders. In: Proceedings of the 16th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer, Volume 2: Workshops, CEUR-WS.org, vol. 2732, pp. 70–73 (2020)

    Google Scholar 

  8. Markowsky, G.: Chain-complete posets and directed sets with applications. Algebra Univ. 6, 53–68 (1976)

    Article  MathSciNet  Google Scholar 

  9. Ogawa, M., Sternagel, C.: Open Induction. Archive of Formal Proofs (2012). https://isa-afp.org/entries/Open_Induction.html

Download references

Author information

Authors and Affiliations

  1. Taras Shevchenko National University of Kyiv, Kyiv, Ukraine

    Ievgen Ivanov

Authors
  1. Ievgen Ivanov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Universität Klagenfurt, Klagenfurt, Austria

    Andreas Bollin

  2. Zaporizhzhia National University, Zaporizhzhia, Ukraine

    Vadim Ermolayev

  3. Universität Klagenfurt, Klagenfurt, Austria

    Heinrich C. Mayr

  4. Taras Shevchenko National University of Kyiv, Kyiv, Ukraine

    Mykola Nikitchenko

  5. Kherson State University, Kherson, Ukraine

    Aleksander Spivakovsky

  6. V. N. Karazin Kharkiv National University, Kharkiv, Ukraine

    Mykola Tkachuk

  7. University of Warmia and Mazury in Olsztyn, Olsztyn, Poland

    Vitaliy Yakovyna

  8. V. N. Karazin Kharkiv National University, Kharkiv, Ukraine

    Grygoriy Zholtkevych

APPENDIX: Isabelle Formalization

APPENDIX: Isabelle Formalization

figure d
figure e
figure f
figure g
figure h
figure i
figure j
figure k
figure l
figure m
figure n
figure o
figure p
figure q
figure r

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ivanov, I. (2021). On Induction Principles for Diamond-Free Partial Orders. In: Bollin, A., et al. Information and Communication Technologies in Education, Research, and Industrial Applications. ICTERI 2020. Communications in Computer and Information Science, vol 1308. Springer, Cham. https://doi.org/10.1007/978-3-030-77592-6_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-77592-6_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-77591-9

  • Online ISBN: 978-3-030-77592-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation