Name
Abstract | ||
|---|---|---|
this paper, we will be concerned with proof assistants that construct a proofobject, i.e. a data structure that explicitly represents the proof of facts established with the system.Proof objects are built by a number of modern proof assistants ([Coq91, Hol92, Lego92]), but theyare rarely used for anything useful. They are generally considered to be exceedingly large anddifficult to understand. On the basis of experiments carried out in the last three years with severalcomputer proof... |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1007/BFb0014048 | TLCA |
Keywords | Field | DocType |
extracting text,data structure,proof assistant | Transducer,Programming language,Computer science,Theoretical computer science,Intelligible form,Mathematical proof,Natural language,Proof assistant | Conference |
ISBN | Citations | PageRank |
3-540-59048-X | 31 | 4.81 |
References | Authors | |
5 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yann Coscoy | 1 | 42 | 6.46 |
| Gilles Kahn | 2 | 1437 | 340.18 |
| Laurent Théry | 3 | 456 | 41.21 |