BriefGPT.xyz
Sep, 2020
在Isabelle/HOL中更快更智能的归纳
Faster Smarter Induction in Isabelle/HOL with SeLFiE
HTML
PDF
Yutaka Nagashima
TL;DR
通过引理归纳在正式验证和数学中发挥了关键作用,但其自动化仍然是计算机科学中长期存在的问题,使用定义量词我们开发了sem_ind,它可以推荐需要通过归纳予以验证的参数
Abstract
proof by induction
is a long-standing challenge in Computer Science. Induction tactics of proof assistants facilitate
proof by induction
, but rely on humans to manually specify how to apply induction. In this pap
→