Whelp

A content based mathematical search engine: Whelp. 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.


References in zbMATH (referenced in 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius: Relational data across mathematical libraries (2019)
  2. Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
  3. Guidi, Ferruccio; Sacerdoti Coen, Claudio: A survey on retrieval of mathematical knowledge (2016)
  4. Guidi, Ferruccio; Sacerdoti Coen, Claudio: A survey on retrieval of mathematical knowledge (2015)
  5. Heras, Jónathan; Komendantskaya, Ekaterina: Recycling proof patterns in Coq: case studies (2014)
  6. Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico: The Matita interactive theorem prover (2011)
  7. Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
  8. Asperti, Andrea; Tassi, Enrico: An interactive driver for goal-directed proof strategies (2009)
  9. Geuvers, H.: Proof assistants: history, ideas and future (2009)
  10. Sacerdoti Coen, Claudio: A user interface for a mathematical system that allows ambiguous formulae (2009)
  11. Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano: User interaction with the Matita proof assistant (2007)
  12. Cairns, Paul; Gow, Jeremy: Integrating searching and authoring in Mizar (2007)
  13. Kaliszyk, Cezary: Web interfaces for proof assistants (2007)
  14. Asperti, Andrea; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano: A content based mathematical search engine: Whelp (2006)