Proof mining with dependent types
- Komendantskaya, E. 1
- Heras, J. 2
-
1
Heriot-Watt University
info
-
2
Universidad de La Rioja
info
ISSN: 0302-9743
Año de publicación: 2017
Volumen: 10383 LNAI
Páginas: 303-318
Tipo: Artículo
Otras publicaciones en: Lecture Notes in Computer Science
Resumen
Several approaches exist to data-mining big corpora of formal proofs. Some of these approaches are based on statistical machine learning, and some - on theory exploration. However, most are developed for either untyped or simply-typed theorem provers. In this paper, we present a method that combines statistical data mining and theory exploration in order to analyse and automate proofs in dependently typed language of Coq. © Springer International Publishing AG 2017.