Zulip Chat Archive

Stream: general

Topic: Isabelle workshop


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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: May 10 2021 at 00:31 UTC