Isabelle workshop

Stream: general

[Gabriel Ebner]

There were two talks now about new search tools for Isabelle, both of them are online if you want to try them out.

• https://search.isabelle.in.tum.de/#search/default_Isabelle2020_AFP2020?page=%5B%5D&q=%7B%22term%22%3A%22complex%20integral%20residue%22%7D
• https://behemoth.cl.cam.ac.uk/search/index.php?id=5efb0cc244050&sid=5efb0cc245a5d&method=method1&query=complex+integral+residue

https://sketis.net/isabelle/isabelle-workshop-2020

[Patrick Massot]

It's great that people are working on this problem. I hope they did interesting things that could benefit all proof assistants. Did it sound very specific to Isabelle?

[Kevin Kappelmann]

I believe the resulting tools are very tightly coupled to Isabelle and its theory export format. They surely will, however, provide good guidance for what seems to work and what probably does not in terms of indexing, relating concepts, search beyond keyword and term pattern matching, and so on for any community interested in these things.

For example, the talk about the SErAPIS tool was quite interesting I'd say: they used Wikipedia articles to obtain keywords for concepts mentioned in Isabelle theory files so that users can search for phrases which are not explicitly mentioned in the theory document.