Angeliki Koutsoukou-Argyraki (Apr 19 2021 at 11:32): Angeliki Koutsoukou-Argyraki (Apr 19 2021 at 11:32):The ALEXANDRIA project is excited to announce the release of the SErAPIS concept-oriented search engine for the Isabelle libraries and AFP 2021.
Homepage: https://behemoth.cl.cam.ac.uk/search/
User Guide: https://behemoth.cl.cam.ac.uk/search/SErAPIS_online_user_guide.pdf
SErAPIS (Search Engine by the ALEXANDRIA Project for ISabelle) is an experimental search engine for Isabelle designed to allow Isabelle users to search and explore the libraries and AFP using keywords and mathematical concepts (natural language phrases that refer to mathematical objects and ideas).
We invite you to try it out. For tips on how to construct effective queries, please see Section 3 of the user guide.
Note that there are 6 different methods to experiment with.
SErAPIS is also a platform for conducting research in novel methods to search Isabelle collections and machine learning in Isabelle.
We kindly ask that you help us with our research by providing us with feedback on the relevance of SErAPIS search results to your searches.
Giving us feedback is optional but very easy to do (see Section 4 of the user guide).
Your feedback will help us:
(i) build data-sets for Isabelle search and machine learning,
(ii) develop new search algorithms for Isabelle collections and;
(iii) develop machine learning methods for aiding the construction of proofs in Isabelle.
All data collected is anonymised.
Thank you,
Yiannos Stathopoulos @Yiannos and Angeliki Koutsoukou-Argyraki.
Kevin Kappelmann (Apr 19 2021 at 12:26):Maybe you want to add this to https://isabelle.systems ? You can add an entry here https://github.com/isabelle-prover/isabelle-prover.github.io :)
Jeremy Avigad (Apr 19 2021 at 15:15):Is it o.k. if I post this to the Lean Zulip group? I am guessing that many in the community there will be happy to experiment with this.
Angeliki Koutsoukou-Argyraki (Apr 19 2021 at 18:23):Sure, please do @Jeremy Avigad --and many thanks for the interest! We would be most grateful for user feedback-- the more feedback the better! Thank you again!
Yiannos (Apr 19 2021 at 18:48):I’d like to point out that:
Methods 1,2,3, 5 and 6 are concept-oriented: they use the input concepts very differently. If one method (default is method 2) is not producing good results in response to the concepts you input, another method might!
Angeliki Koutsoukou-Argyraki (Apr 19 2021 at 21:29):NB: The last indexing of the Archive of Formal Proofs was done on 23/2/2021, so AFP entries after that date are not included. We will be re-indexing every now and then so as to be as up-to-date as possible!
Angeliki Koutsoukou-Argyraki (Apr 19 2021 at 21:48):Many thanks for the suggestion @Kevin Kappelmann , I just created a pull request--hope it looks ok!
Jeremy Avigad (Apr 19 2021 at 21:57):Done!
Max Kirchmeier (Apr 26 2021 at 08:21):That's a cool project!
I would like to point out a (minor) naming collision, however: https://github.com/ejgallego/coq-serapi
I'm not sure how much of an issue it really is, since the SerAPI project is so far still fairly unknown/small (and lives in the disjoint Coq universe anyway), but I wanted to mention it.
Angeliki Koutsoukou-Argyraki (May 05 2021 at 22:12):Thank you for letting us know @Max Kirchmeier . We weren't aware of this--luckily the names are not the same, though very similar. Hopefully there won't be any confusion as the Coq project is not a search engine. In our case, SErAPIS stands for "Search Engine by the Alexandria Project for ISabelle" and it is an intended pun referring to the deity "Serapis" (see e.g. wiki) once worshipped in Alexandria--which is the name of our ERC project--inspired by the Library of Alexandria in Egypt, since we are working with libraries of formal proofs :) https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/
Last updated: Apr 24 2024 at 08:20 UTC