Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings
Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings
复制标题
自动扣除 - CADE 28 - 第 28 届自动扣除国际会议，虚拟活动，2021 年 7 月 12-15 日，会议记录
DOI：
10.1007/978-3-030-79876-5_21
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Hozzová P
中科院分区：
文献类型：
--
作者：
Hozzová P
整数在编程中无处不在，因此也在程序分析和验证的应用中。这样的应用程序通常需要某种归纳推理。在本文中，我们分析了自动化归纳推理与整数的挑战。我们引入整数归纳推理规则的饱和框架内的一阶定理证明。我们在定理证明器Vampire中实现了这些规则，并将我们的工作与其他最先进的定理证明器进行了比较。我们的研究结果表明，我们的方法解决新的问题来自程序分析和整数的数学性质的强度。
Integers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the theorem prover Vampire and evaluated our work against other state-of-the-art theorem provers. Our results demonstrate the strength of our approach by solving new problems coming from program analysis and mathematical properties of integers.