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

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

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.