演绎综合理论探索
Theory Exploration Powered By Deductive Synthesis
摘要：
近年来，经过验证的软件数量大幅增长。复杂性质的证明现在可以使用高阶理论和微积分来实现。复杂的性质导致了越来越多的定义和相关引理，它们构成了证明构造的一个组成部分。在此之后--无论是自动的还是半自动的--计算机辅助引理发现的方法已经出现。在这项工作中，我们引入了一个新的符号技术自下而上的引理发现，也就是说，从一个基本的归纳数据类型和递归定义集的引理库的生成。这被称为理论探索问题，到目前为止，已经提出了基于反例生成或更流行的随机测试与一阶求解器相结合的解决方案。我们的新方法，是纯粹的演绎，消除了随机测试作为一个过滤阶段和SMT求解器的需要。因此，它适合于组合推理和处理用户定义的高阶函数。我们的实现已经示出找到比现有技术更多的引理，同时避免冗余。
英文摘要：
Recent years have seen tremendous growth in the amount of verified software. Proofs for complex properties can now be achieved using higher-order theories and calculi. Complex properties lead to an ever-growing number of definitions and associated lemmas, which constitute an integral part of proof construction. Following this -- whether automatic or semi-automatic -- methods for computer-aided lemma discovery have emerged. In this work, we introduce a new symbolic technique for bottom-up lemma discovery, that is, the generation of a library of lemmas from a base set of inductive data types and recursive definitions. This is known as the theory exploration problem, and so far, solutions have been proposed based either on counter-example generation or the more prevalent random testing combined with first-order solvers. Our new approach, being purely deductive, eliminates the need for random testing as a filtering phase and for SMT solvers. Therefore it is amenable compositional reasoning and for the treatment of user-defined higher-order functions. Our implementation has shown to find more lemmas than prior art, while avoiding redundancy.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
