Advances in Artificial Intelligence - 9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I
Advances in Artificial Intelligence - 9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I
复制标题
人工智能的进展 - 第九届墨西哥国际人工智能会议，MICAI 2010，墨西哥帕丘卡，2010 年 11 月 8-13 日，会议记录，第一部分
DOI：
10.1007/978-3-642-16761-4_31
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Montano-Rivas O
中科院分区：
文献类型：
--
作者：
Montano-Rivas O
我们描述了一种自动发明/探索新的数学理论的方法，其目标是产生与人类产生的结果相当的结果，例如，在Isabelle证明助理的图书馆中。我们的方法是基于“方案”，这是高阶逻辑中的术语。我们表明，可以自动化方案的实例化过程来生成猜想和定义。我们还展示了在理论探索过程中发现的新定义和引理如何不仅可以用于帮助探索过程中的证明义务，而且还可以减少大多数理论形成系统中固有的冗余。我们在一个名为isasscheme的自动化工具中实现了我们的想法，该工具采用了Knuth-Bendix完井和最新的自动归纳证明工具。我们已经用自然数理论和列表理论评估了我们的系统。
We describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle proof assistant. Our approach is based on ‘schemes’, which are terms in higher-order logic. We show that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. We also show how the new definitions and the lemmata discovered during the exploration of the theory can be used not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory formation systems. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.