IsaPlanner: A Prototype Proof Planner in Isabelle
IsaPlanner: A Prototype Proof Planner in Isabelle
复制标题
DOI：
10.1007/978-3-540-45085-6_22
复制
发表时间：
2003-07
期刊：
影响因子：
--
通讯作者：
L. Dixon;Jacques D. Fleuriot
中科院分区：
文献类型：
--
作者：
L. Dixon;Jacques D. Fleuriot
IsaPlanner是交互式定理证明器Isabelle中用于证明规划的通用框架。它方便了推理技术的编码，可用于自动猜想和证明定理。本文介绍了我们的方法证明规划，给出了和概述IsaPlanner，并提出了一个简单而有效的推理技术。
IsaPlanneris a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. This paper introduces our approach to proof planning, gives and overview ofIsaPlanner, and presents one simple yet effective reasoning technique.