Mining the Archive of Formal Proofs. (English) Zbl 1417.68176
Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 3-17 (2015).
Summary: 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.
For the entire collection see [Zbl 1316.68015].
For the entire collection see [Zbl 1316.68015].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68U35 | Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) |
Software:
Mizar; z3; Isabelle/HOL; Isabelle; SPASS; Sledgehammer; VAMPIRE; MML; MPTP 0.2; Archive Formal Proofs; HOLyHammer; E Theorem ProverReferences:
| [1] | The Mizar mathematical library. http://mizar.org · Zbl 1278.68290 |
| [2] | An, Y.; Janssen, J.; Milios, E., Characterizing and mining citation graphs of the computer science literature, Knowl. Inf. Syst., 6, 664-678 (2004) · doi:10.1007/s10115-003-0128-3 |
| [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 · Zbl 1356.68178 |
| [4] | Blanchette, JC; Böhme, S.; Paulson, LC, Extending Sledgehammer with SMT solvers, J. Autom. Reason., 51, 1, 109-128 (2013) · Zbl 1314.68272 · doi:10.1007/s10817-013-9278-5 |
| [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 · Zbl 1386.68149 |
| [6] | Böhme, S.; Nipkow, T.; Giesl, J.; Hähnle, R., Sledgehammer: judgement day, Automated Reasoning, 107-121 (2010), Heidelberg: Springer, Heidelberg · Zbl 1291.68327 · doi:10.1007/978-3-642-14203-1_9 |
| [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) |
| [8] | Church, A., A formulation of the simple theory of types, J. Symb. Logic, 5, 2, 56-68 (1940) · JFM 66.1192.06 · doi:10.2307/2266170 |
| [9] | Crovella, ME; Bestavros, A., Self-similarity in world wide web traffic: evidence and possible causes, IEEE/ACM Trans. Network., 5, 6, 835-846 (1997) · doi:10.1109/90.650143 |
| [10] | de Moura, L.; Bjørner, NS; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24 |
| [11] | Gonthier, G.; Blazy, S.; Paulin-Mohring, C.; Pichardie, D., A machine-checked proof of the odd order theorem, Interactive Theorem Proving, 163-179 (2013), Heidelberg: Springer, Heidelberg · Zbl 1317.68211 · doi:10.1007/978-3-642-39634-2_14 |
| [12] | Hölzl, J.; Immler, F.; Huffman, B.; Blazy, S.; Paulin-Mohring, C.; Pichardie, D., Type classes and filters for mathematical analysis in Isabelle/HOL, Interactive Theorem Proving, 279-294 (2013), Heidelberg: Springer, Heidelberg · Zbl 1317.68213 · doi:10.1007/978-3-642-39634-2_21 |
| [13] | Kaliszyk, C.; Urban, J., HOL(y)Hammer: online ATP service for HOL light, Math. Comput. Sci., 9, 1, 5-22 (2015) · Zbl 1322.68177 · doi:10.1007/s11786-014-0182-0 |
| [14] | Lammich, P.; Lochbihler, A.; Kaufmann, M.; Paulson, LC, The Isabelle collections framework, Interactive Theorem Proving, 339-354 (2010), Heidelberg: Springer, Heidelberg · Zbl 1291.68357 · doi:10.1007/978-3-642-14052-5_24 |
| [15] | Leroy, X., A formally verified compiler back-end, J. Autom. Reason., 43, 363-446 (2009) · Zbl 1185.68215 · doi:10.1007/s10817-009-9155-4 |
| [16] | Lochbihler, A.; Seidl, H., Java and the Java memory model — a unified, machine-checked formalisation, Programming Languages and Systems, 497-517 (2012), Heidelberg: Springer, Heidelberg · Zbl 1352.68034 · doi:10.1007/978-3-642-28869-2_25 |
| [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) |
| [18] | Matuszewski, R.; Rudnicki, P., Mizar: the first 30 years, Mech. Math. Appl., 4, 1, 3-24 (2005) |
| [19] | Meng, J.; Paulson, LC, Lightweight relevance filtering for machine-generated resolution problems, J. Appl. Logic, 7, 1, 41-57 (2009) · Zbl 1183.68560 · doi:10.1016/j.jal.2007.07.004 |
| [20] | Nipkow, T.; Klein, G., Concrete Semantics with Isabelle/HOL (2014), Heidelberg: Springer, Heidelberg · Zbl 1410.68004 |
| [21] | Nipkow, T.; Paulson, LC; Wenzel, M., Isabelle/HOL (2002), Heidelberg: Springer, Heidelberg · Zbl 1097.68632 |
| [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., 15, 2-3, 91-110 (2002) · Zbl 1021.68082 |
| [24] | Schulz, S.; McMillan, K.; Middeldorp, A.; Voronkov, A., System description: E 1.8, Logic for Programming, Artificial Intelligence, and Reasoning, 735-743 (2013), Heidelberg: Springer, Heidelberg · Zbl 1407.68442 · doi:10.1007/978-3-642-45221-5_49 |
| [25] | Staples, M.; Jeffery, R.; Andronick, J.; Murray, T.; Klein, G.; Kolanski, R.; Morisio, M.; Dybå, T.; Torchiano, M., Productivity for proof engineering, Empirical Software Engineering and Measurement (ESEM 2014), 15:1-15:4 (2014), New York: ACM, New York |
| [26] | Urban, J., MPTP 0.2: design, implementation, and initial experiments, J. Autom. Reason., 37, 1-2, 21-43 (2006) · Zbl 1113.68095 |
| [27] | Urban, J.; Rudnicki, P.; Sutcliffe, G., ATP and presentation service for Mizar formalizations, J. Autom. Reason., 50, 2, 229-241 (2013) · Zbl 1260.68380 · doi:10.1007/s10817-012-9269-y |
| [28] | Weidenbach, C.; Dimova, D.; Fietzke, A.; Kumar, R.; Suda, M.; Wischnewski, P.; Schmidt, RA, SPASS version 3.5, Automated Deduction - CADE-22, 140-145 (2009), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-02959-2_10 |
| [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) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
