数学知识形式化为双形理论图的案例研究
Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study
摘要：
双形式理论是公理理论和算法理论的结合，支持推理和计算的集成。这些对于形式化处理数学表达式的算法是理想的。理论图是一个理论网络，由保意义的理论态射连接，将一个理论的公式映射到另一个理论的公式。理论图反过来非常适合于使用最方便的词汇表在最方便的抽象层次上形式化数学知识。我们感兴趣的问题是，一个机构的数学知识是否可以有效地形式化为一个理论图的biform理论。作为一个测试案例，我们看一下编码自然数算术的理论图。我们使用了两种不同的形式来做这件事，我们描述和比较。第一个是在${\rm CTT}_{\rm uqe}$中实现的，这是Church的类型论的一个版本，带有引用和评估，第二个是在Agda中实现的，这是一种依赖类型的程序设计语言。
英文摘要：
A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for formalizing algorithms that manipulate mathematical expressions. A theory graph is a network of theories connected by meaning-preserving theory morphisms that map the formulas of one theory to the formulas of another theory. Theory graphs are in turn well suited for formalizing mathematical knowledge at the most convenient level of abstraction using the most convenient vocabulary. We are interested in the problem of whether a body of mathematical knowledge can be effectively formalized as a theory graph of biform theories. As a test case, we look at the graph of theories encoding natural number arithmetic. We used two different formalisms to do this, which we describe and compare. The first is realized in ${\rm CTT}_{\rm uqe}$, a version of Church's type theory with quotation and evaluation, and the second is realized in Agda, a dependently typed programming language.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
