Welcome to SErAPIS

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.

In order to meet the above objectives, we store some cookies and collect anonymised information. Please see our privacy statement here.

We have prepared two short videos to get you started with using SErAPIS:

For detailed instructions on how to use SErAPIS and to help us meet our objectives, please see the user guide.

SErAPIS is developed by the ALEXANDRIA Project at the University of Cambridge and is supported by the European Research Council (ERC)

News and Updates

  • 31/5/2021: Date of last indexing.
  • 19/6/2021: Major update!
    • Index updated to include AFP from 31/05/2021.
    • Two new concept-oriented search algorithms: method 7 and 8 (now default).
    • Better matching for fact names entered as keywords.
    • Speed improvements.
  • 21/4/2021: Made small improvement to keyword search.
  • 19/4/2021: Public release.
  • 23/2/2021: Date of first indexing.

Notes

  • We have have eight search methods (algorithms) available to you. Feel free to try alternative methods if the default does not give you any results of interest
  • Methods 1,2,3,5, 6, 7 and 8 are concept-oriented methods: they use input concepts differently when trying to satisfy your queries. If one of these methods is not producing good results in response to the concepts you input, another method might.
  • Method 4 is keyword-based only and will not accept concepts as input.

SErAPIS: Search Engine by the ALEXANDRIA Project for ISabelle, University of Cambridge, 2020-2021.