Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1007/978-3-319-62075-6_21 | INTELLIGENT COMPUTER MATHEMATICS |
Keywords | DocType | Volume |
Interactive theorem proving, Coq, Dependent types, Tactics, Machine learning, Clustering, Theory exploration | Conference | 10383 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
12 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ekaterina Komendantskaya | 1 | 150 | 22.66 |
| Jónathan Heras | 2 | 94 | 23.31 |