论文标题
FindFacts：可扩展定理搜索
FindFacts: A Scalable Theorem Search
论文作者
论文摘要
伊莎贝尔（Isabelle）的正式证明档案（AFP）已于2019年底增长到500多篇文章。与此同时，发现其形式化并没有变得更加容易。在撰写本文时，特定网站的AFP Google搜索和Isabelle Find_theores resp。 Find_consts命令（仅在导入理论上起作用）仍然是唯一可以使用Isabelle中正式化的工具。我们提出了Findfacts，这是一种针对正式Isabelle理论内容的新型域特异性搜索工具。我们没有使用术语统一，而是通过经典的钻孔搜索引擎解决了问题。我们特别强调搜索系统的可扩展性，以便可以进行交互式搜索整个AFP。
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.
