MATHsAiD: Automated mathematical theory exploration
MATHsAiD: Automated mathematical theory exploration
复制标题
MATHsAiD：自动化数学理论探索
DOI：
10.1007/s10489-017-0954-8
复制
发表时间：
2017
影响因子：
5.3
通讯作者：
McCasland R
中科院分区：
文献类型：
--
作者：
McCasland R
MATHsAiD 项目的目标是构建一个自动发现定理的工具；设计和构建一个工具，根据一组用户提供的公理和定义自动推测和证明定理（引理、推论等）。不需要其他输入。例如，该工具允许数学家尝试特定定义的多个版本，并且在相对较短的时间内，能够根据得出的定理看到每个版本的一些结果。此外，自动发现的定理也许可以帮助用户自己发现和证明进一步的定理。该工具还可以很容易地被教育工作者（例如生成练习集）和学生使用。以类似的方式，它也可能有助于自动定理证明者通过自动生成证明者所需的引理来分派软件验证中出现的许多更困难的证明义务，以完成这些证明。
The aim of the MATHsAiD project is to build a tool for automated theorem-discovery; to design and build a tool to automatically conjecture and prove theorems (lemmas, corollaries, etc.) from a set of user-supplied axioms and definitions. No other input is required. This tool would, for instance, allow a mathematician to try several versions of a particular definition, and in a relatively small amount of time, be able to see some of the consequences, in terms of the resulting theorems, of each version. Moreover, the automatically discovered theorems could perhaps help the users to discover and prove further theorems for themselves. The tool could also easily be used by educators (to generate exercise sets, for instance) and by students as well. In a similar fashion, it might also prove useful in enabling automated theorem provers to dispatch many of the more difficult proof obligations arising in software verification, by automatically generating lemmas which are needed by the prover, in order to finish these proofs.
登录
查看更多内容
通用代数中的简单应用题††本文报告的工作得到了美国海军研究办公室的部分支持。
DOI：
--
发表时间：
1970
期刊：
影响因子：
--
作者：
D. Knuth;P. Bendix
通讯作者：
P. Bendix
Rippling - 数学推理的元级指导
DOI：
10.1017/cbo9780511543326
发表时间：
2005
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
A. Bundy;D. Basin;D. Hutter;Andrew Ireland
通讯作者：
Andrew Ireland
DOI：
10.1007/978-3-540-45085-6_22
发表时间：
2003-07
期刊：
--
影响因子：
--
作者：
L. Dixon;Jacques D. Fleuriot
通讯作者：
L. Dixon;Jacques D. Fleuriot
拉卡托斯式推理的计算模型
DOI：
10.1007/3-540-48834-0
发表时间：
2007
期刊：
The Mathematical Gazette
影响因子：
--
作者：
A. Pease
通讯作者：
A. Pease
DOI：
--
发表时间：
1991
期刊：
Computational Logic - Essays in Honor of Alan Robinson
影响因子：
--
作者：
A. Bundy
通讯作者：
A. Bundy