A content based mathematical search engine: Whelp

Andrea Asperti; Ferruccio Guidi; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli

doi:10.1007/11617990_2

A content based mathematical search engine: Whelp

Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli

University of Bologna

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Types for Proofs and Programs - International Workshop, TYPES 2004, Revised Selected Papers
Pages	17-32
Number of pages	16
DOIs	https://doi.org/10.1007/11617990_2
Publication status	Published - 23 Jun 2006
Externally published	Yes
Event	International Workshop on Types for Proofs and Programs, TYPES 2004 - Jouy-en-Josas, France Duration: 15 Dec 2004 → 18 Dec 2004

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3839 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Workshop on Types for Proofs and Programs, TYPES 2004
Country/Territory	France
City	Jouy-en-Josas
Period	15/12/04 → 18/12/04

Access to Document

10.1007/11617990_2

Cite this

Asperti, A., Guidi, F., Coen, C. S., Tassi, E., & Zacchiroli, S. (2006). A content based mathematical search engine: Whelp. In Types for Proofs and Programs - International Workshop, TYPES 2004, Revised Selected Papers (pp. 17-32). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3839 LNCS). https://doi.org/10.1007/11617990_2

@inproceedings{102676e0cd7b4e3ba3f911e6e0f78dc2,

title = "A content based mathematical search engine: Whelp",

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.",

author = "Andrea Asperti and Ferruccio Guidi and Coen, \{Claudio Sacerdoti\} and Enrico Tassi and Stefano Zacchiroli",

year = "2006",

month = jun,

day = "23",

doi = "10.1007/11617990\_2",

language = "English",

isbn = "3540314288",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "17--32",

booktitle = "Types for Proofs and Programs - International Workshop, TYPES 2004, Revised Selected Papers",

note = "International Workshop on Types for Proofs and Programs, TYPES 2004 ; Conference date: 15-12-2004 Through 18-12-2004",

}

Asperti, A, Guidi, F, Coen, CS, Tassi, E & Zacchiroli, S 2006, A content based mathematical search engine: Whelp. in Types for Proofs and Programs - International Workshop, TYPES 2004, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3839 LNCS, pp. 17-32, International Workshop on Types for Proofs and Programs, TYPES 2004, Jouy-en-Josas, France, 15/12/04. https://doi.org/10.1007/11617990_2

A content based mathematical search engine: Whelp. / Asperti, Andrea; Guidi, Ferruccio; Coen, Claudio Sacerdoti et al.
Types for Proofs and Programs - International Workshop, TYPES 2004, Revised Selected Papers. 2006. p. 17-32 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3839 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A content based mathematical search engine

T2 - International Workshop on Types for Proofs and Programs, TYPES 2004

AU - Asperti, Andrea

AU - Guidi, Ferruccio

AU - Coen, Claudio Sacerdoti

AU - Tassi, Enrico

AU - Zacchiroli, Stefano

PY - 2006/6/23

Y1 - 2006/6/23

N2 - 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.

AB - 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.

U2 - 10.1007/11617990_2

DO - 10.1007/11617990_2

M3 - Conference contribution

AN - SCOPUS:33745137062

SN - 3540314288

SN - 9783540314288

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 17

EP - 32

BT - Types for Proofs and Programs - International Workshop, TYPES 2004, Revised Selected Papers

Y2 - 15 December 2004 through 18 December 2004

ER -

Asperti A, Guidi F, Coen CS, Tassi E, Zacchiroli S. A content based mathematical search engine: Whelp. In Types for Proofs and Programs - International Workshop, TYPES 2004, Revised Selected Papers. 2006. p. 17-32. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11617990_2

A content based mathematical search engine: Whelp

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this