Hipster: Integrating Theory Exploration in a Proof Assistant
Hipster: Integrating Theory Exploration in a Proof Assistant
复制标题
Hipster：将理论探索整合到证明助手中
DOI：
10.1007/978-3-319-08434-3_9
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Koen Claessen
中科院分区：
文献类型：
--
作者：
Moa Johansson;Dan Rosén;Nicholas Smallbone;Koen Claessen
本文描述了一个将理论探索与证明助手isabelle/hol探索的系统。用于在新理论开发中自动生成有关一组数据类型和功能的基本引理。发现缺失的引理，可以证明当前的目标。 。
This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new interesting lemmas in a given theory development. Hipster can be used in two main modes. The first is exploratory mode, used for automatically generating basic lemmas about a given set of datatypes and functions in a new theory development. The second is proof mode, used in a particular proof attempt, trying to discover the missing lemmas which would allow the current goal to be proved. Hipster’s proof mode complements and boosts existing proof automation techniques that rely on automatically selecting existing lemmas, by inventing new lemmas that need induction to be proved. We show example uses of both modes.
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
MaSh：Sledgehammer 的机器学习
DOI：
10.1007/978-3-642-39634-2_6
发表时间：
2013
期刊：
影响因子：
--
作者：
Daniel Kühlwein;Jasmin Christian Blanchette;Cezary Kaliszyk;Josef Urban
通讯作者：
Josef Urban