Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System
Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System
复制标题
交互式定理证明的自动理论探索：- Hipster 系统简介
DOI：
10.1007/978-3-319-66107-0_1
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Moa Johansson
中科院分区：
文献类型：
--
作者：
Moa Johansson
理论探索（Theory Exploration）是一种利用测试自动发现数学理论开发中新的有趣引理的技术。本文将介绍一个理论探索系统Hipster，它能自动发现和证明Isabelle/HOL中关于给定数据集和函数集的引理。Hipster的开发最初的动机是试图为归纳证明提供更高水平的自动化。自动化归纳证明是棘手的，尤其是因为它们经常需要辅助引理，而这些引理本身需要通过归纳来证明。我们发现，许多这样的基本引理可以通过理论探索自动发现，重要的是，足够快地与交互式定理证明器结合使用，而不会使用户感到无聊。
Theory exploration is a technique for automatically discovering new interesting lemmas in a mathematical theory development using testing. In this paper I will present the theory exploration system Hipster, which automatically discovers and proves lemmas about a given set of datatypes and functions in Isabelle/HOL. The development of Hipster was originally motivated by attempts to provide a higher level of automation for proofs by induction. Automating inductive proofs is tricky, not least because they often need auxiliary lemmas which themselves need to be proved by induction. We found that many such basic lemmas can be discovered automatically by theory exploration, and importantly, quickly enough for use in conjunction with an interactive theorem prover without boring the user.
DOI：
10.1016/j.eswa.2011.06.055
发表时间：
2012-02
期刊：
Expert Syst. Appl.
影响因子：
--
作者：
Omar Montano-Rivas;R. McCasland;L. Dixon;A. Bundy
通讯作者：
Omar Montano-Rivas;R. McCasland;L. Dixon;A. Bundy