Mining the archive of formal proofs

Jasmin Christian Blanchette; Maximilian Haslbeck; Daniel Matichuk; Tobias Nipkow

doi:10.1007/978-3-319-20615-8_1

Mining the archive of formal proofs

Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

32 Scopus citations

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.

Original language	English
Title of host publication	Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings
Editors	Manfred Kerber, Volker Sorge, Florian Rabe, Jacques Carette, Cezary Kaliszyk
Publisher	Springer Verlag
Pages	3-17
Number of pages	15
ISBN (Print)	9783319206141
DOIs	https://doi.org/10.1007/978-3-319-20615-8_1
State	Published - 2015
Event	International Conference on Intelligent Computer Mathematics, CICM 2015 - Washington, United States Duration: 13 Jul 2015 → 17 Jul 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9150
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Intelligent Computer Mathematics, CICM 2015
Country/Territory	United States
City	Washington
Period	13/07/15 → 17/07/15

Access to Document

10.1007/978-3-319-20615-8_1

Cite this

Blanchette, J. C., Haslbeck, M., Matichuk, D., & Nipkow, T. (2015). Mining the archive of formal proofs. In M. Kerber, V. Sorge, F. Rabe, J. Carette, & C. Kaliszyk (Eds.), Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings (pp. 3-17). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9150). Springer Verlag. https://doi.org/10.1007/978-3-319-20615-8_1

Blanchette, Jasmin Christian ; Haslbeck, Maximilian ; Matichuk, Daniel et al. / Mining the archive of formal proofs. Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. editor / Manfred Kerber ; Volker Sorge ; Florian Rabe ; Jacques Carette ; Cezary Kaliszyk. Springer Verlag, 2015. pp. 3-17 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6474c81ee41b4acab5449bde6a29b1e4,

title = "Mining the archive of formal proofs",

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.",

author = "Blanchette, {Jasmin Christian} and Maximilian Haslbeck and Daniel Matichuk and Tobias Nipkow",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; International Conference on Intelligent Computer Mathematics, CICM 2015 ; Conference date: 13-07-2015 Through 17-07-2015",

year = "2015",

doi = "10.1007/978-3-319-20615-8_1",

language = "English",

isbn = "9783319206141",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "3--17",

editor = "Manfred Kerber and Volker Sorge and Florian Rabe and Jacques Carette and Cezary Kaliszyk",

booktitle = "Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings",

}

Blanchette, JC, Haslbeck, M, Matichuk, D & Nipkow, T 2015, Mining the archive of formal proofs. in M Kerber, V Sorge, F Rabe, J Carette & C Kaliszyk (eds), Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9150, Springer Verlag, pp. 3-17, International Conference on Intelligent Computer Mathematics, CICM 2015, Washington, United States, 13/07/15. https://doi.org/10.1007/978-3-319-20615-8_1

Mining the archive of formal proofs. / Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel et al.
Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. ed. / Manfred Kerber; Volker Sorge; Florian Rabe; Jacques Carette; Cezary Kaliszyk. Springer Verlag, 2015. p. 3-17 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9150).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 - http://www.scopus.com/inward/record.url?scp=84949934968&partnerID=8YFLogxK

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 -

Blanchette JC, Haslbeck M, Matichuk D, Nipkow T. Mining the archive of formal proofs. In Kerber M, Sorge V, Rabe F, Carette J, Kaliszyk C, editors, Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. Springer Verlag. 2015. p. 3-17. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-20615-8_1

Mining the archive of formal proofs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this