Bridging the gap between the human mathematical language and unambiguous computer representations

弥合人类数学语言和明确的计算机表示之间的差距

• 批准号: 2770826
• 金额: --
• 依托单位: Heriot-Watt University
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2022
• 资助国家: 英国
• 起止时间: 2022 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2770826
• 关键词: Bridging; gap; between; human; mathematical

This project will improve capabilities for converting between the common mathematical language (CML), the mixture of natural language text and symbolic formulas of human-written mathematics, and unambiguous computer representations of mathematics suitable for use in computer systems for mathematics (CSMs). Existing CSMs generally treat the textual portion of mathematics as uninterpreted blobs of data. Computer proof assistants (e.g., Isabelle) have the potential to represent the semantic content of CML texts, but are hard to learn, have input languages that are quite distant from CML, and have generally committed to technical choices (in logics, types, and foundations) that can conflict with the choices made by a CML text. This project aims to bridge the gap between CML texts and the input languages of proof assistants by developing (1) software and methodology for parsing and disambiguating CML, (2) unambiguous representations for recording the results of this parsing and disambiguation, and (3) connections between these representations and proof assistants. Research will investigate questions of how best to resolve ambiguity and determine bindings, what discourse representation formalism or logic is most suitable, how best to handle implicit information, and a number of other issues. The work will build on recent progress in grammars for CML, types for CML, dynamic parsing, discourse representation logics, controlled natural languages (CNLs) for CML, and machine learning for searching CML. We will develop new techniques for using partial proving for disambiguation and new representations for disambiguated CML. Many of the pieces are already available and a PhD-sized work package has good potential to overcome obstacles and put them together. The expected results have the potential to make many CSMs more accessible and could enhance the production and use of mathematics in many ways.

该项目将提高公共数学语言（CML）、自然语言文本和人类书写的数学符号公式的混合以及适合于计算机数学系统（csm）使用的数学的明确计算机表示之间的转换能力。现有的csm通常将数学的文本部分视为未解释的数据块。计算机证明助手（例如Isabelle）有潜力表示CML文本的语义内容，但很难学习，其输入语言与CML相距甚远，并且通常致力于与CML文本所做的选择相冲突的技术选择（在逻辑，类型和基础方面）。该项目旨在通过开发(1)解析和消歧CML的软件和方法，(2)记录解析和消歧结果的无歧义表示，以及(3)这些表示与证明助手之间的联系，弥合CML文本与证明助手的输入语言之间的差距。研究将探讨如何最好地解决歧义和确定绑定，什么话语表示形式主义或逻辑是最合适的，如何最好地处理隐式信息，以及许多其他问题。这项工作将建立在CML语法、CML类型、动态解析、话语表示逻辑、CML控制自然语言（cnl）和CML搜索机器学习的最新进展之上。我们将开发用于消歧的部分证明和消歧CML的新表示的新技术。许多部分已经可用，并且博士大小的工作包具有克服障碍并将它们组合在一起的良好潜力。预期的结果有可能使许多csm更容易获得，并可以在许多方面加强数学的产生和使用。