Article

Mining the Archive of Formal Proofs

Authors:

Jasmin Christian Blanchette,

Maximilian Haslbeck,

Daniel Matichuk,

Tobias NipkowAuthors Info & Claims

Proceedings of the International Conference on Intelligent Computer Mathematics - Volume 9150

Pages 3 - 17

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

Published: 13 July 2015 Publication History

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.

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

Digital Library

[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

Digital Library

[4]

Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 511, 109---128 2013

[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

Digital Library

[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

Digital Library

[8]

Church, A.: A formulation of the simple theory of types. J. Symb. Logic 52, 56---68 1940

[9]

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

Digital Library

[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

Digital Library

[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

Digital Library

[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

Digital Library

[13]

Kaliszyk, C., Urban, J.: HOLyHammer: online ATP service for HOL light. Math. Comput. Sci. 91, 5---22 2015

[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

Digital Library

[15]

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

Digital Library

[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

Digital Library

[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

Digital Library

[18]

Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mech. Math. Appl. 41, 3---24 2005

[19]

Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 71, 41---57 2009

[20]

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

Digital Library

[21]

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

[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

[23]

Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 152---3, 91---110 2002

Digital Library

[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

[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

Digital Library

[26]

Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 371---2, 21---43 2006

Digital Library

[27]

Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 502, 229---241 2013

Digital Library

[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

Digital Library

[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. 1831, 137---151 2009

Cited By

Sutcliffe GDesharnais M(2024)The CADE-29 Automated Theorem Proving System Competition – CASC-29AI Communications10.3233/AIC-23032537:4(485-503)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.3233/AIC-230325
MacKenzie CHuch FVaughan JFleuriot J(2022)Re-imagining the Isabelle Archive of Formal ProofsIntelligent Computer Mathematics10.1007/978-3-031-16681-5_11(162-167)Online publication date: 19-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16681-5_11
Huch F(2022)Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal ProofsIntelligent Computer Mathematics10.1007/978-3-031-16681-5_10(147-161)Online publication date: 19-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16681-5_10
Show More Cited By

Recommendations

Logic of Negation-Complete Interactive Proofs (Formal Theory of Epistemic Deciders)

We produce a decidable classical normal modal logic of internalised negation-complete and thus disjunctive non-monotonic interactive proofs (LDiiP) from an existing logical counterpart of non-monotonic or instant interactive proofs (LiiP). LDiiP ...
Formal SOS-Proofs for the Lambda-Calculus

We describe in this paper formalisations for the properties of weakening, type-substitutivity, subject-reduction and termination of the usual big-step evaluation relation. Our language is the lambda-calculus whose simplicity allows us to show actual ...
Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)

We produce a decidable super-intuitionistic normal modal logic of internalised intuitionistic (and thus disjunctive and monotonic) interactive proofs (LIiP) from an existing classical counterpart of classical monotonic non-disjunctive interactive proofs ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Proceedings of the International Conference on Intelligent Computer Mathematics - Volume 9150

July 2015

344 pages

ISBN:9783319206141

Editors:
Manfred Kerber
School of Computer Science, University of Birmingham, Birmingham, United Kingdom
,
Jacques Carette
McMaster University, Hamilton, Canada
,
Cezary Kaliszyk
University of Innsbruck, Innsbruck, Austria
,
Florian Rabe
Jacobs University Bremen, Bremen, Germany
,
Volker Sorge
University of Birmingham, Birmingham, United Kingdom

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 13 July 2015

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sutcliffe GDesharnais M(2024)The CADE-29 Automated Theorem Proving System Competition – CASC-29AI Communications10.3233/AIC-23032537:4(485-503)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.3233/AIC-230325
MacKenzie CHuch FVaughan JFleuriot J(2022)Re-imagining the Isabelle Archive of Formal ProofsIntelligent Computer Mathematics10.1007/978-3-031-16681-5_11(162-167)Online publication date: 19-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16681-5_11
Huch F(2022)Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal ProofsIntelligent Computer Mathematics10.1007/978-3-031-16681-5_10(147-161)Online publication date: 19-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16681-5_10
Wang QBrown CKaliszyk CUrban JBlanchette JHriţcu C(2020)Exploration of neural machine translation in autoformalization of mathematics in MizarProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373827(85-98)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373827
The mathlib Community Blanchette JHriţcu C(2020)The lean mathematical libraryProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373824(367-381)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373824
Ringer TSanchez-Stern AGrossman DLerner SBlanchette JHriţcu C(2020)REPLica: REPL instrumentation for Coq analysisProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373823(99-113)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373823
Nagashima Y(2020)Simple Dataset for Proof Method Recommendation in Isabelle/HOLIntelligent Computer Mathematics10.1007/978-3-030-53518-6_21(297-302)Online publication date: 26-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-53518-6_21
Nawaz MSun MFournier-Viger P(2019)Proof Guidance in PVS with Sequential Pattern MiningFundamentals of Software Engineering10.1007/978-3-030-31517-7_4(45-60)Online publication date: 1-May-2019
https://dl.acm.org/doi/10.1007/978-3-030-31517-7_4
Brucker AWolff B(2019)Isabelle/DOF: Design and ImplementationSoftware Engineering and Formal Methods10.1007/978-3-030-30446-1_15(275-292)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30446-1_15
Nagashima YHe YHuchard MKästner CFraser G(2018)PaMpeR: proof method recommendation system for Isabelle/HOLProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238210(362-372)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238210
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents