Abstract
SErAPIS ( Search Engine by the ALEXANDRIA Project for ISabelle) is a research search engine for the Isabelle 2021 and Archive of Formal Proofs 2021 libraries.
The main objectives of SErAPIS are:
to provide search functionality for Isabelle users that does not rely on syntactically complex pattern matching. Instead, SErAPIS is concept-oriented: the search engine tries to understand the mathematical ideas and topic behind a user's enquiry.
to provide search that doesn't rely on the loaded libraries or theories at each session. SErAPIS searches all libraries and AFP using a pre-computed index.
to enable research in Isabelle search. We aim to build a data set that will allow researchers to develop and evaluate retrieval models for mathematical facts in Isabelle.
Available on https://behemoth.cl.cam.ac.uk/search/
The main objectives of SErAPIS are:
to provide search functionality for Isabelle users that does not rely on syntactically complex pattern matching. Instead, SErAPIS is concept-oriented: the search engine tries to understand the mathematical ideas and topic behind a user's enquiry.
to provide search that doesn't rely on the loaded libraries or theories at each session. SErAPIS searches all libraries and AFP using a pre-computed index.
to enable research in Isabelle search. We aim to build a data set that will allow researchers to develop and evaluate retrieval models for mathematical facts in Isabelle.
Available on https://behemoth.cl.cam.ac.uk/search/
| Original language | English |
|---|---|
| Type | Software: Search Engine |
| Media of output | Online |
| Publication status | Published - 19 Apr 2021 |