论文标题
定义性量化符实现语义推理，以归纳
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
论文作者
论文摘要
证明助手提供了通过归纳来应用证明的策略，但是这些策略依赖于人类工程师给出的意见。为了使这一艰辛的过程自动化，我们开发了自拍照，这是一种布尔人查询语言，以代表经验丰富的用户在Isabelle/Hol中应用归纳策略的知识：当我们应用自拍照的归纳启发式启发式启发式启发式问题时，将归纳问题和参数归入归纳策略时，自拍解释者对该问题的结构是否相关，是否与该问题相关，是否可以遵守该问题，是否符合该问题的结构，是否可以使用该问题来进行统治。常数。为了检查句法分析与恒定定义分析之间的复杂相互作用，我们介绍了定义性量词。为了进行评估，我们使用自拍照来建立自动归纳鄙分。我们基于347个归纳问题的评估表明，我们的新摊子在1.0秒的超时时间内提高了1.4 x 10^3％的提高，而加速的中位数为4.48 x。
Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a boolean query language to represent experienced users' knowledge on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct tactic, the SeLFiE interpreter judges whether the arguments are plausible for that problem according to the heuristic by examining both the syntactic structure of the problem and definitions of the relevant constants. To examine the intricate interaction between syntactic analysis and analysis of constant definitions, we introduce definitional quantifiers. For evaluation we build an automatic induction prover using SeLFiE. Our evaluation based on 347 inductive problems shows that our new prover achieves 1.4 x 10^3% improvement over the corresponding baseline prover for 1.0 second of timeout and the median value of speedup is 4.48x.
