Skip to main content
Springer Nature Link
Log in

Formalizing O Notation in Isabelle/HOL

  • Conference paper
Automated Reasoning (IJCAR 2004)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 3097))

Included in the following conference series:

Abstract

We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

References

  1. Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete mathematics: a foundation for computer science, 2nd edn. Addison-Wesley Publishing Company, Reading (1994)

    MATH  Google Scholar 

  2. Kammüller, F., Wenzel, M., Paulson, L.C.: Locales – a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, p. 149. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Krueger, R., Rudnicki, P., Shelley, P.: Asymptotic notation. Part I: theory. Journal of Formalized Mathematics 11 (1999), http://mizar.org/JFM/Vol11/asympt_0.html

  4. Krueger, R., Rudnicki, P., Shelley, P.: Asymptotic notation. Part II: examples and problems. Journal of Formalized Mathematics 11 (1999), http://mizar.org/JFM/Vol11/asympt_1.html

  5. Nathanson, M.B.: Elementary Methods in Number Theory. Springer, New York (2000)

    MATH  Google Scholar 

  6. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

  7. Shapiro, H.N.: Introduction to the theory of numbers. Pure and Applied Mathematics. John Wiley & Sons Inc., New York (1983), A Wiley-Interscience Publication

    MATH  Google Scholar 

  8. Wenzel, M.: Using axiomatic type classes in Isabelle (1995), http://www.cl.cam.ac.uk/Research/HVG/Isabelle/docs.html

  9. Type classes and overloading in higher-order logic. In: Gunther, E., Felty, A. (eds.) TPHOLs 1997, pp. 307–322. Murray Hill, New Jersey (1997)

    Google Scholar 

  10. Wenzel, M., Bauer, G.: Calculational reasoning revisited (an Isabelle/ Isar experience). In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 75–90. Springer, Heidelberg (2001)

    Google Scholar 

  11. The Coq proof assistant. Developed by the LogiCal project, http://pauillac.inria.fr/coq/coq-eng.html

  12. The Isabelle theorem proving environment. Developed by Larry Paulson at Cambridge University and Tobias Nipkow at TU Munich, http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University,  

    Jeremy Avigad & Kevin Donnelly

Authors
  1. Jeremy Avigad
    View author publications

    Search author on:PubMed Google Scholar

  2. Kevin Donnelly
    View author publications

    Search author on:PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Information Security Group, Dep. of Computer Science, ETH, Zurich, Switzerland

    David Basin

  2. LORIA & INRIA Lorraine UMR 7503,  

    Michaël Rusinowitch

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Avigad, J., Donnelly, K. (2004). Formalizing O Notation in Isabelle/HOL. In: Basin, D., Rusinowitch, M. (eds) Automated Reasoning. IJCAR 2004. Lecture Notes in Computer Science(), vol 3097. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25984-8_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-25984-8_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22345-0

  • Online ISBN: 978-3-540-25984-8

  • eBook Packages: Springer Book Archive

Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Publish with us

Policies and ethics