Name
Abstract | ||
|---|---|---|
Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophistication, the re-use of libraries by non-experts or across domains is a challenge. In this paper, we provide detailed case studies and evaluate the machine-learning tool ML4PG built to interactively data-mine the electronic libraries of proofs, and to provide user guidance on the basis of proof patterns found in the existing libraries. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/s11786-014-0173-1 | Mathematics in Computer Science |
Keywords | Field | DocType |
Interactive theorem proving, Coq, SSReflect, Machine learning, Clustering | Theorem provers,Discrete mathematics,Programming language,Computer science,Theoretical computer science,Mathematical proof,Cluster analysis,Sophistication,Proof assistant | Journal |
Volume | Issue | ISSN |
8 | 1 | 1661-8270 |
Citations | PageRank | References |
7 | 0.52 | 27 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jónathan Heras | 1 | 94 | 23.31 |
| Ekaterina Komendantskaya | 2 | 150 | 22.66 |