Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Announcing SErAPIS: a new search engine for Is...


view this post on Zulip Email Gateway (Apr 19 2021 at 11:14):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
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.

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 and Angeliki Koutsoukou-Argyraki.

view this post on Zulip Email Gateway (Apr 19 2021 at 13:28):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
PS. We would like to highlight that there are 6 different methods
available for you to try out.

Many thanks again for your valuable feedback.

With kind regards,

Yiannos and Angeliki

view this post on Zulip Email Gateway (Apr 20 2021 at 08:48):

From: "Yiannos A. Stathopoulos" <yas23@cam.ac.uk>
A quick addendum:

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!


Last updated: Dec 05 2021 at 22:18 UTC