Second-order Automated Deduction

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

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.