KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings
KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings
复制标题
KI 2019：人工智能进展 - 第 42 届德国人工智能会议，德国卡塞尔，2019 年 9 月 23-26 日，会议记录
DOI：
10.1007/978-3-030-30179-8_6
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Ayers E
中科院分区：
文献类型：
--
作者：
Ayers E
我们引入了一个全自动系统，在精益定理证明器中实现，可以解决日常数学的等式问题。我们设计该系统的首要任务是它应该以类似于人类的方式构建平等证明。第二个目标是它使用的方法应该与领域无关。系统的基本策略是使用子任务堆栈进行操作：每当没有明确的方法来实现堆栈顶部的任务时，程序就会找到一个有前途的子任务，例如重写子项，并将其放置在堆栈的顶部。启发式指导有希望的子任务的选择和重写过程。通过以人类的方式将问题分解为任务，使得证明更加人性化。我们证明，我们的系统可以简单地证明等式定理，而无需像标准定理证明器那样预先选择或定向重写规则，也无需调用重型工具来执行简单推理。
We introduce a fully automatic system, implemented in the Lean theorem prover, that solves equality problems of everyday mathematics. Our overriding priority in devising the system is that it should construct proofs of equality in a way that is similar to that of humans. A second goal is that the methods it uses should be domain independent. The basic strategy of the system is to operate with a subtask stack: whenever there is no clear way of making progress towards the task at the top of the stack, the program finds a promising subtask, such as rewriting a subterm, and places that at the top of the stack instead. Heuristics guide the choice of promising subtasks and the rewriting process. This makes proofs more human-like by breaking the problem into tasks in the way that a human would. We show that our system can prove equality theorems simply, without having to preselect or orient rewrite rules as in standard theorem provers, and without having to invoke heavy duty tools for performing simple reasoning.