A Small Experiement in Event-b Rippling
A Small Experiement in Event-b Rippling
复制标题
Event-b 涟漪中的一个小实验
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
L. Dixon
中科院分区：
文献类型：
--
作者：
G. Grov;A. Bundy;L. Dixon
虽然Rodin中的许多POs是自动排出的，但仍有大量POs需要用户输入——在许多情况下，专家可以很容易地看到如何完成证明。此外，在许多情况下，相同的“想法”适用于多个POs，从而创建POs家族（具有类似的证明策略）。在我们新启动的AI4FM项目中，目标是通过依靠专家干预来执行一个证明来实现更高程度的自动化，这将使证明者能够在同一家族中释放其他证明。具体来说，我们希望构建一种工具，能够从一次证明尝试中学习到足够的知识，从而提高自动证明“相似”结果的机会。我们的核心目标是找到能够减少证明中的搜索空间的高级策略。我们的假设是：
Although many POs in Rodin are discharged automatically, a large number still require user input – and in many cases, an expert can easily see how to complete a proof. Moreover, in many cases the same “idea” applies to several of the POs, thus creating families of POs (with a similar proof strategy). In our newly started AI4FM project the goal is to achieve a higher degree of automation by relying on expert intervention to carry out one proof, where this would enable a prover to discharge the others in the same family. Specifically, we hope to build a tool that will learn enough from one proof attempt to improve the chances of proving “similar” results automatically. Central to our goal is that we find high-level strategies capable of cutting down the search space in proofs. Our hypothesis is: