The HR Program for Theorem Generation
The HR Program for Theorem Generation
复制标题
定理生成的人力资源计划
DOI：
10.1007/3-540-45620-1_24
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
S. Colton
中科院分区：
文献类型：
--
作者：
S. Colton
自动化理论的形成涉及产生感兴趣的对象，这些对象的概念，概念与概念的概念和证明。等等，这些猜想包括含义和唯一的猜想，如果证明了这些猜测，则将其变为定理，如果不证实，则非理论类似于Zhang的MCS程序[11]。数学家Hardy和Ramanujan - 在数学领域中进行理论形成。水獭定理证明[8]可以证明猜想的域，水獭和狼牙棒有效，人力资源可以产生大量的定理，用于测试自动化定理的侵略（ATPS），或者较小的素数暗示，这代表了一些基本事实在一个领域中，我们在§2中解释了人力资源的运作方式，并在§3中进行了代表性会议。对于自动定理证明，以及用于ATP系统的TPTP测试问题库的基准定理[10]。 Simonco/Research/HR。
Automated theory formation involves the production of objects of interest, concepts about those objects, conjectures relating the concepts and proofs of the conjectures. In group theory, for example, the objects of interest are the groups themselves, the concepts include element types, subgroup types, etc., the conjectures include implication and if-and-only-if conjectures and these become theorems if they are proved, non-theorems if disproved. Similar to Zhang’s MCS program [11], the HR system [1] — named after mathematicians Hardy and Ramanujan — performs theory formation in mathematical domains. It works by (i) using the MACE model generator [9] to generate objects of interest from axiom sets (ii) performing the concept formation and conjecture making itself and (iii) using the Otter theorem prover [8] to prove conjectures. In domains where Otter and MACE are effective, HR can produce large numbers of theorems for testing automated theorem provers (ATPs), or smaller numbers of prime implicates, which represent some of the fundamental facts in a domain. We explain how HR operates in §2 and give details of a representative session in §3. As discussed in §4, the applications of HR to automated reasoning include the generation of constraints for constraint satisfaction problems, the generation of lemmas for automated theorem proving, and the production of benchmark theorems for the TPTP library of test problems for ATP systems [10]. HR is a Java program available for download here: http://www.dai.ed.ac.uk/~simonco/research/hr.