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.