Applied Mathematical Logic

应用数理逻辑

• 批准号: 9704520
• 负责人: Kenneth Kunen
• 金额: $ 18万
• 依托单位: University of Wisconsin-Madison
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-05-15 至 2001-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9704520&HistoricalAwards=false
• 关键词: Applied; Mathematical; Logic

Research will be conducted on automated reasoning, on mathematics, and on the use of automated reasoning (AR) techniques to solve mathematical problems. The "pure" mathematics topics include investigations into set theopy, topology, and measure theory. The properties of the standard (Lebesgue) measure on the real numbers are well understood, but various generalizations of Lebesgue measure lead to interesting open questions. The proposer plans further work on measure extension axioms, which involve extending Lebesgue measure to measure additional (non-measurable) sets of real numbers. He also plans to consider measures on other topological spaces. The "pure" AR topics include improving the technology for linked resolution and automatic lemma generation. In addition, a number of topics involve integrating AR and mathematics by using AR to derive mathematical theorems. In particular, it is proposed to continue work on algebraic systems such as quasigroups and loops; one specific project here is to find a structure theory for G-loops. It is also proposed to work on single axioms for groups. Besides these specific questions in algebra, it is planned to look at the general problem of transcribing machine-generated proofs into meaningful form. Work is also proposed on verification systems, which are designed to use a computer to check the correctness of existing mathematics. There are three distinct, but related, threads to this research. The first thread involves the expansion of our knowledge of traditional pure mathematics, without any specific practical application in mind. The other two involve automated peasoning (AR) tools. AR allows the computer to derive logical conclusions from given knowledge. This subject has been in existence since the 1960s, but it is only in recent years that the tools have become powerful enough to discover conclusions which could not have been discovered without human assistance. The second thread involves a continuation of the proposer's work in impr oving the AR tools and using these tools to create new results in mathematics. This is of interest not only for the mathematics itself, but because it demonstrates the power of the tools, which can then be applied to reasoning tasks in other areas of science and engineering, as well as to autonomous decision making by robotic agents. The third thread involves verification systems; these systems do not discover new mathematics, but rather are used as an automated database to collect and verify existing mathematics. One potential application to advanced mathematics is the use of the computer as a referee to validate new mathematical results. On the more elementary level, these tools can provide an accessible intelligent database of mathematical knowledge, which can be accessed by users of mathematics. The difference between this and traditional database methods in cataloging mathematics is that the computer has "understood" and verified the knowledge it has, so that the the knowledge may be accessed by idea or concept, rather than by keywords.

将对自动推理，数学以及使用自动推理（AR）技术来解决数学问题的研究。 “纯”数学主题包括对集体理论，拓扑和测量理论的研究。 对实数的标准（Lebesgue）度量的属性得到了充分的理解，但是Lebesgue测度的各种概括导致了有趣的开放问题。 提议者计划进一步研究衡量扩展公理的工作，该公理涉及扩展Lebesgue度量以衡量额外的（不可衡量的）实数。 他还计划考虑对其他拓扑空间的措施。 “纯” AR主题包括改进链接分辨率和自动引理生成的技术。 此外，许多主题涉及通过使用AR得出数学定理来整合AR和数学。 特别是，有人建议继续在代数系统（例如准元素和循环）上进行工作。这里的一个特定项目是找到G循环的结构理论。 还建议在组上为组上的单个公理工作。 除了代数中的这些特定问题外，还计划研究将机器生成的证据转录为有意义的形式的总体问题。 还提出了有关验证系统的工作，该验证系统旨在使用计算机检查现有数学的正确性。 这项研究有三个不同但相关的线程。 第一个线程涉及我们对传统纯数学知识的扩展，而没有任何特定的实际应用。 另外两个涉及自动化（AR）工具。 AR允许计算机从给定的知识中得出逻辑结论。 自1960年代以来，这个主题一直存在，但是直到近年来，这些工具才变得足够强大，可以发现没有人类援助就无法发现的结论。 第二个线程涉及提议者的工作，以改善AR工具，并使用这些工具来创建数学上的新结果。 这不仅对于数学本身而言，而且是因为它展示了工具的力量，然后可以将其应用于科学和工程其他领域的推理任务，以及机器人代理商的自主决策。 第三个线程涉及验证系统；这些系统不会发现新的数学，而是用作自动化数据库，以收集和验证现有数学。 高级数学的一种潜在应用是使用计算机作为裁判来验证新的数学结果。 在更基本的层面上，这些工具可以提供数学知识的智能数据库，该数据库可以由数学用户访问。 该数学分类中的该数据库方法与传统数据库方法之间的区别在于，计算机已经“理解”并验证了其知识，以便可以通过思想或概念而不是通过关键字来访问知识。