TY - GEN
T1 - Mining the archive of formal proofs
AU - Blanchette, Jasmin Christian
AU - Haslbeck, Maximilian
AU - Matichuk, Daniel
AU - Nipkow, Tobias
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84949934968
U2 - 10.1007/978-3-319-20615-8_1
DO - 10.1007/978-3-319-20615-8_1
M3 - Conference contribution
AN - SCOPUS:84949934968
SN - 9783319206141
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 17
BT - Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings
A2 - Kerber, Manfred
A2 - Sorge, Volker
A2 - Rabe, Florian
A2 - Carette, Jacques
A2 - Kaliszyk, Cezary
PB - Springer Verlag
T2 - International Conference on Intelligent Computer Mathematics, CICM 2015
Y2 - 13 July 2015 through 17 July 2015
ER -