The Isabelle Archive of Formal Proofs (AFP) has grown to over 500 articles in late 2019. Meanwhile, finding formalizations in it has not exactly become easier. At the time of writing, the site-specific AFP google search and the Isabelle find_theories resp. find_consts commands (that only work on imported theories) are still the only tools readily available to find formalizations in Isabelle. We present FindFacts, a novel domain-specific search tool for formal Isabelle theory content. Instead of utilizing term unification, we solve the problem with a classical drill-down search engine. We put special emphasis on scalability of the search system, so that the whole AFP can be searched interactively.
翻译:伊莎贝尔正式证据档案(AFP)在2019年后期已发展到500多篇文章。 同时,在其中找到正式内容并没有变得非常容易。 在撰写本报告时,针对特定网站的AFP谷歌搜索和Isabelle find_theories resp. find_conts 命令(仅涉及进口理论的工作)仍然是在伊莎贝尔找到正式内容的唯一现成工具。 我们为正式的伊莎贝尔理论内容展示了“发现事实”这个新颖的域域搜索工具。 我们不是使用术语统一,而是用经典的自下计搜索引擎解决问题。 我们特别强调搜索系统的可扩展性, 以便可以交互搜索整个 AFP 。