Second-order Automated Deduction

二阶自动扣除

• 批准号: 0204362
• 负责人: Michael Beeson
• 金额: $ 18.81万
• 依托单位: San Jose State University Foundation
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-07-01 至 2006-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0204362&HistoricalAwards=false
• 关键词: Second; order; Automated; Deduction

ABSTRACT0204362Beeson, MichaelSan Jose State Univ FdnThis award will enhance the theorem-prover Otter to cope better with second-order logic. It will use this enhanced version of Otter to formalize a small amount of elementary number theory, a small amount of set theory, and theorems about the cardinality of finite sets, as required to proceed to theorems in group theory as usually presented in an undergraduate course in algebra, up to and perhaps (but not necessarily) including the Sylow theorems. It will also enhance Otter by adding a capability for polynomial simplification, which in turn will enable it to proceed further in number theory. Although first-order group theory has been a source of many test problems for automated deduction, the material in an undergraduate course typically begins with theorems about subgroups and homomorphisms, and uses the concept of a prime number, so second-order logic (or set theory) and induction are essential ingredients to even sophomore-level mathematics. It is high time that theorem-provers be made able to cope with these fundamental areas of mathematics, which are naturally multi-sorted (elements, numbers, functions, and sets) and second-order (elements, cosets, subgroups).The long-term aim of automated deduction is to make the computer useful as a "mathematician's assistant". The goal is that the computer could check proofs, filling in any missing details, and verify their correctness. Perhaps the computer could carry out some of the simpler parts of the mathematics mechanically. Maybe (in the distant future) the computer might even prove interesting new theorems on a regular basis. At present computers can be used for some kinds of calculations, but their use for helping with proofs is in its infancy, in spite of half a century of research. Part of the problem is the richness of mathematical language; part of the problem is the complicated relationship between calculations and proofs; and part of the problem is the "needle-in-the-haystack" difficulty of finding a proof or disproof of an unsolved conjecture. Otter is a theorem-proving program developed at Argonne National Laboratories. This research will provide some enhancements to Otter that should help it deal with the "richness of language" problem and the "calculations within proofs" problem. To test the effectiveness of our efforts, the PI will try to "computerize" some theorems in mathematics that are usually taught in the sophomore or junior year to mathematics majors. These are theorems in an area of mathematics called "group theory", which usually comes after calculus and is widely used in many branches of mathematics and physics. Many of the theorems found in the first course in this subject have so far resisted attempts to get computers to prove them.

摘要0204362Beeson，Michael圣何塞州立大学Fdn该奖项将增强定理证明者Otter以更好地应对二阶逻辑。它将使用 Otter 的增强版本来形式化少量的初等数论、少量的集合论以及关于有限集基数的定理，按照需要进行群论定理（通常在代数本科课程中介绍），直到可能（但不一定）包括 Sylow 定理。 它还将通过添加多项式简化功能来增强 Otter，这反过来又使其能够在数论方面进一步发展。 尽管一阶群论一直是许多自动演绎测试问题的来源，但本科课程中的材料通常从有关子群和同态的定理开始，并使用素数的概念，因此二阶逻辑（或集合论）和归纳法甚至是大二数学的基本成分。现在是时候让定理证明者能够应对这些数学基本领域了，这些领域自然是多排序的（元素、数字、函数和集合）和二阶（元素、陪集、子群）。自动演绎的长期目标是使计算机成为“数学家的助手”。 目标是计算机可以检查证据，填写任何缺失的细节，并验证其正确性。 也许计算机可以机械地执行一些更简单的数学部分。 也许（在遥远的未来）计算机甚至可能定期证明有趣的新定理。 目前，计算机可以用于某些类型的计算，但尽管经过了半个世纪的研究，它们在帮助证明方面的应用仍处于起步阶段。 部分问题在于数学语言的丰富性； 部分问题在于计算和证明之间的复杂关系；部分问题在于，要找到未解决的猜想的证据或反驳，就像大海捞针一样困难。 Otter 是阿贡国家实验室开发的定理证明程序。这项研究将为 Otter 提供一些增强功能，帮助其处理“语言的丰富性”问题和“证明内的计算”问题。 为了测试我们努力的有效性，PI将尝试将一些通常在大二或大三向数学专业教授的数学定理“计算机化”。 这些是数学领域中称为“群论”的定理，通常出现在微积分之后，并广泛应用于数学和物理学的许多分支。 迄今为止，在本主题的第一门课程中发现的许多定理都未能通过计算机来证明它们。