Skip to main content
SpringerLink
Log in
Book cover

International Conference on Intelligent Computer Mathematics

CICM 2015: Intelligent Computer Mathematics pp 3–17Cite as

Mining the Archive of Formal Proofs

  • Conference paper
  • First Online:

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

Abstract

The Archive of Formal Proofs is a vast collection of computer-checked proofs developed using the proof assistant Isabelle. We perform an in-depth analysis of the archive, looking at various properties of the proof developments, including size, dependencies, and proof style. This gives some insights into the nature of formal proofs.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Notes

  1. 1.

    http://www21.in.tum.de/~blanchet/afp_mining_data.tgz.

References

  1. The Mizar mathematical library. http://mizar.org

  2. An, Y., Janssen, J., Milios, E.: Characterizing and mining citation graphs of the computer science literature. Knowl. Inf. Syst. 6, 664–678 (2004)

    Article  Google Scholar 

  3. Blanchette, J.C., Böhme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. Accepted in J. Autom. Reason. http://www21.in.tum.de/~blanchet/isar2.pdf

  4. Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  5. Blanchette, J.C., Greenaway, D., Kaliszyk, C., Kühlwein, D., Urban, J.: A learning-based relevance filter for Isabelle/HOL (2015) (Submitted). http://www21.in.tum.de/~blanchet/mash2.pdf

  6. Böhme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 107–121. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA\(^ \text{+ } \) proof system: building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, p. 44. Springer, Heidelberg (2010)

    Google Scholar 

  8. Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5(2), 56–68 (1940)

    Article  MathSciNet  MATH  Google Scholar 

  9. Crovella, M.E., Bestavros, A.: Self-similarity in world wide web traffic: evidence and possible causes. IEEE/ACM Trans. Network. 5(6), 835–846 (1997)

    Article  Google Scholar 

  10. de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279–294. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  13. Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5–22 (2015)

    Article  MATH  Google Scholar 

  14. Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 339–354. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43, 363–446 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  16. Lochbihler, A.: Java and the Java memory model — a unified, machine-checked formalisation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 497–517. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  17. Matichuk, D., Murray, T., Andronick, J., Jeffery, R., Klein, G., Staples, M.: Empirical study towards a leading indicator for cost of formal software verification. In: Canfora, G., Elbaum, S. (eds.) International Conference on Software Engineering (ICSE 2015). ACM (2015)

    Google Scholar 

  18. Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mech. Math. Appl. 4(1), 3–24 (2005)

    Google Scholar 

  19. Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 7(1), 41–57 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  20. Nipkow, T., Klein, G.: Concrete Semantics with Isabelle/HOL. Springer, Heidelberg (2014). http://concrete-semantics.org

    MATH  Google Scholar 

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

    MATH  Google Scholar 

  22. Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) International Workshop on the Implementation of Logics (IWIL 2010). EPiC Series, vol. 2, pp. 1–11. EasyChair (2012)

    Google Scholar 

  23. Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 15(2–3), 91–110 (2002)

    MATH  Google Scholar 

  24. Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  25. Staples, M., Jeffery, R., Andronick, J., Murray, T., Klein, G., Kolanski, R.: Productivity for proof engineering. In: Morisio, M., Dybå, T., Torchiano, M. (eds.) Empirical Software Engineering and Measurement (ESEM 2014), pp. 15:1–15:4. ACM, New York (2014)

    Google Scholar 

  26. Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1–2), 21–43 (2006)

    MATH  Google Scholar 

  27. Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229–241 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  28. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  29. Wenzel, M.: Isabelle/Isar—a versatile environment for human-readable formal proof documents. Ph.D. thesis, Institut für Informatik, Technische Universität München (2002). http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html

  30. Wiedijk, F.: Statistics on digital libraries of mathematics. Stud. Logic, Gramm. Rhetor. 18(31), 137–151 (2009)

    Google Scholar 

Download references

Acknowledgement

Our colleague Johannes Hölzl suggested the proof depth diagram (Fig. 5), which we found insightful. Matichuk is partially supported by NICTA. NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program. Nipkow is supported by DFG grant NI 491/16-1.

Author information

Authors and Affiliations

  1. Inria Nancy and LORIA, Villers-lès-Nancy, France

    Jasmin Christian Blanchette

  2. Max-Planck-Institut Für Informatik, Saarbrücken, Germany

    Jasmin Christian Blanchette

  3. Fakultät für Informatik, Technische Universität München, Munich, Germany

    Maximilian Haslbeck & Tobias Nipkow

  4. NICTA, Sydney, Australia

    Daniel Matichuk

  5. University of New South Wales, Sydney, Australia

    Daniel Matichuk

Authors
  1. Jasmin Christian Blanchette
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maximilian Haslbeck
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Daniel Matichuk
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tobias Nipkow
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tobias Nipkow .

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Birmingham, Birmingham, United Kingdom

    Manfred Kerber

  2. McMaster University, Hamilton, Ontario, Canada

    Jacques Carette

  3. University of Innsbruck, Innsbruck, Austria

    Cezary Kaliszyk

  4. Jacobs University Bremen, Bremen, Germany

    Florian Rabe

  5. University of Birmingham, Birmingham, United Kingdom

    Volker Sorge

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T. (2015). Mining the Archive of Formal Proofs. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds) Intelligent Computer Mathematics. CICM 2015. Lecture Notes in Computer Science(), vol 9150. Springer, Cham. https://doi.org/10.1007/978-3-319-20615-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-20615-8_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-20614-1

  • Online ISBN: 978-3-319-20615-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation