Scheme-based theorem discovery and concept invention
Scheme-based theorem discovery and concept invention
复制标题
DOI：
10.1016/j.eswa.2011.06.055
复制
发表时间：
2012-02
期刊：
影响因子：
--
通讯作者：
Omar Montano-Rivas;R. McCasland;L. Dixon;A. Bundy
中科院分区：
文献类型：
--
作者：
Omar Montano-Rivas;R. McCasland;L. Dixon;A. Bundy
我们描述了一种自动发明/探索新数学理论的方法，目标是产生可与人类产生的结果相媲美的结果，例如，在Isabelle证明助手的库中所示。我们的方法是基于“方案”，这是高阶逻辑中的公式。我们证明了自动化方案的实例化过程以生成猜想和定义是可能的。我们还展示了如何使用在探索理论过程中发现的新定义和引理，不仅有助于探索过程中的证明义务，而且还可以减少大多数理论形成系统中固有的冗余。我们使用有序重写的结合交换(AC)算子来避免相同实例化的AC变化。我们在一个自动化工具ISASCHEME中实现了我们的想法，该工具使用了Knuth-Bendex完备化和最近的自动归纳证明工具。我们已经用自然数理论和列表理论评估了我们的系统。
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 formulae 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 a 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 exploit associative-commutative (AC) operators using ordered rewriting to avoid AC variations of the same instantiation. 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.