Name
Abstract | ||
|---|---|---|
The prototype of a content based search engine for mathematical knowledge supporting a small set of queries requiring matching and/or typing operations is described. The prototype — called Whelp — exploits a metadata approach for indexing the information that looks far more flexible than traditional indexing techniques for structured expressions like substitution, discrimination, or context trees. The prototype has been instantiated to the standard library of the Coq proof assistant extended with many user contributions. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/11617990_2 | TYPES |
Keywords | Field | DocType |
traditional indexing technique,mathematical search engine,small set,mathematical knowledge,context tree,typing operation,standard library,search engine,metadata approach,coq proof assistant,structured expression,indexation | Metadata,Search engine,Expression (mathematics),Computer science,Search engine indexing,Type theory,Algorithm,Exploit,Metadata modeling,Proof assistant | Conference |
Volume | ISSN | ISBN |
3839 | 0302-9743 | 3-540-31428-8 |
Citations | PageRank | References |
25 | 1.69 | 14 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andrea Asperti | 1 | 849 | 75.19 |
| Ferruccio Guidi | 2 | 90 | 10.72 |
| Claudio Sacerdoti Coen | 3 | 384 | 40.66 |
| Enrico Tassi | 4 | 327 | 21.79 |
| Stefano Zacchiroli | 5 | 426 | 37.60 |
| CS Coen | 6 | 29 | 2.31 |