Applied Mathematical Logic

研究将进行自动推理，数学和使用自动推理（AR）技术来解决数学问题。“纯”数学主题包括对集合论、拓扑学和测度论的研究。标准（勒贝格）测度在实数上的性质已被很好地理解，但对勒贝格测度的各种推广导致了有趣的开放性问题。提议者计划进一步研究测度扩展公理，包括将勒贝格测度扩展到测度额外的（不可测量的）实数集。他还计划考虑其他拓扑空间上的措施。“纯”AR主题包括改进链接分辨率和自动引理生成技术。此外，许多主题涉及通过使用AR推导数学定理来整合AR和数学。特别地，建议继续研究代数系统，如拟群和环路；这里的一个具体项目是找到g环的结构理论。它也被提议对群的单一公理进行研究。除了代数中的这些具体问题外，还计划研究将机器生成的证明转化为有意义的形式的一般问题。还提出了验证系统的工作，该系统旨在使用计算机来检查现有数学的正确性。这项研究有三个不同但相关的线索。第一条线索涉及我们对传统纯数学知识的扩展，没有任何具体的实际应用。另外两个涉及自动化操作（AR）工具。AR允许计算机从给定的知识中得出逻辑结论。这门学科自20世纪60年代以来一直存在，但直到最近几年，这些工具才变得强大到足以发现没有人类帮助就无法发现的结论。第二条线索涉及提议者在改进AR工具和使用这些工具创建数学新结果方面的工作的延续。这不仅对数学本身感兴趣，而且因为它展示了这些工具的强大功能，这些工具可以应用于其他科学和工程领域的推理任务，以及机器人代理的自主决策。第三条线索涉及核查制度；这些系统并不发现新的数学，而是用作收集和验证现有数学的自动化数据库。高等数学的一个潜在应用是使用计算机作为裁判来验证新的数学结果。在更初级的层面上，这些工具可以提供一个可访问的智能数学知识数据库，可供数学用户访问。这与传统的数学编目数据库方法的不同之处在于，计算机已经“理解”并验证了它所拥有的知识，因此可以通过思想或概念而不是通过关键词来访问知识。

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.