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.
A.Asperti, F.Guidi, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli (2005). A content based mathematical search engine: Whelp. s.l : Springer.
A content based mathematical search engine: Whelp
ASPERTI, ANDREA;GUIDI, FERRUCCIO;SACERDOTI COEN, CLAUDIO;TASSI, ENRICO;ZACCHIROLI, STEFANO
2005
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
