Applied Mathematical Logic

研究将进行自动推理，数学，以及使用自动推理（AR）技术来解决数学问题。 “纯”数学的主题包括调查集theopy，拓扑学和测量理论。 真实的数上的标准（勒贝格）测度的性质是很好理解的，但是勒贝格测度的各种推广导致了有趣的公开问题。 提议者计划进一步的工作措施扩展公理，其中涉及扩展勒贝格措施，以衡量额外的（非可测）集的真实的数字。 他还计划考虑其他拓扑空间的措施。 “纯”AR主题包括改进链接解析和自动词元生成技术。 此外，许多主题涉及通过使用AR导出数学定理来整合AR和数学。 特别是，它建议继续工作的代数系统，如拟群和循环;一个具体的项目在这里是找到一个结构理论的G-循环。 它还建议工作的单一公理的群体。 除了代数中的这些具体问题之外，还计划研究将机器生成的证明转换为有意义的形式的一般问题。 工作也提出了验证系统，这是设计使用计算机来检查现有的数学的正确性。 这项研究有三个不同但相关的线索。 第一条线索涉及扩展我们对传统纯数学的知识，没有任何具体的实际应用。 另外两个涉及自动化peasoning（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.