University of Cambridge > Talks.cam > Artificial Intelligence Research Group Talks (Computer Laboratory) > Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language : Technical Challenges

Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language : Technical Challenges

Add to your list(s) Download to your calendar using vCal

  • UserYiannos Stathopoulos and Angeliki Koutsoukou-Argyraki
  • ClockTuesday 02 June 2020, 13:15-14:15
  • HouseOnline on Teams.

If you have a question about this talk, please contact Mateja Jamnik.

ONLINE link

We introduce SErAPIS (: Search Engine by the Alexandria Project for ISabelle), a work-in-progress search engine for the Isabelle libraries. SErAPIS uses an offline index (all libraries are indexed a-priori) that enables library search using natural language and does not rely on the loaded libraries. We describe the SErAPIS pipeline that indexes Isabelle facts by associating them to words and concepts (special phrases that refer to mathematical structures, objects and ideas) in Wikipedia mathematics articles. We also describe three models for extracting textual descriptions of facts from these articles and present a preliminary experiment with four retrieval models based on our indexing methods. We are planning several further developments to the engine as well as an extensive evaluation using online user data.

This talk is part of the Artificial Intelligence Research Group Talks (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity