Second-order Automated Deduction

这个奖项将提高定理证明者水獭更好地科普二阶逻辑。它将使用这个增强版本的水獭正式少量的初等数论，少量的集合论，和定理的基数有限集，需要进行定理群论通常在代数本科课程，直到可能（但不一定）包括西洛定理。 它还将通过增加多项式简化的能力来增强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.