Zulip Chat Archive

Stream: general

Topic: Isabelle workshop


Gabriel Ebner (Jun 30 2020 at 10:19):

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

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

Patrick Massot (Jun 30 2020 at 22:13):

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 (Jun 30 2020 at 22:29):

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.


Last updated: Dec 20 2023 at 11:08 UTC