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 with two objectives:
- Collect queries and relevance decisions to build a data set for eloping and evaluating Isabelle retrieval algorithms (also known as a
test collection
. - Understand the requirements and behaviour of Isabelle search users (in an anonymised manner).
SErAPIS is designed to be an easy-to-use search engine for Isabelle 2021 and AFP2021.
The idea is that you (the user) can use natural language keywords and phrases that represent mathematical concepts to find what you are looking for in the libraries, rather than syntactically complex patterns.
SErAPIS tries to understand
the topic of what you are looking for and present relevant results.
For further information about SErAPIS please see our paper.
SErAPIS is developed by the ALEXANDRIA Project at the University of Cambridge and is supported by the European Research Council (ERC)
