一种通用的二分法
A Universal Machine for Biform Theory Graphs
摘要：
广义地说，数学语义辅助系统主要有两类：证明助手用逻辑表达语义，强调推理;计算机代数系统用程序设计语言表达语义，强调计算。一段时间以来，结合两种方法的互补优势，同时弥补它们的互补弱点，一直是机械化数学界的一个重要目标。我们拿起的想法，biform理论和解释它在MMTt/OMDoc框架，介绍了基础理论的方法，因此可以代表逻辑和程序设计语言的理论。这就产生了一个正式的，模块化的框架，biform理论图混合规范和实现共享模块系统和类型信息。我们提出了自动化的知识管理工作流程，接口到现有的规范/编程工具，并启用OpenMath机器，可操作的biform理论，评估表达式通过详尽地应用各自的运营商的实现。我们通过将实现添加到OpenMath标准内容字典来评估新的biform框架。
英文摘要：
Broadly speaking, there are two kinds of semantics-aware assistant systems for mathematics: proof assistants express the semantic in logic and emphasize deduction, and computer algebra systems express the semantics in programming languages and emphasize computation. Combining the complementary strengths of both approaches while mending their complementary weaknesses has been an important goal of the mechanized mathematics community for some time. We pick up on the idea of biform theories and interpret it in the MMTt/OMDoc framework which introduced the foundations-as-theories approach, and can thus represent both logics and programming languages as theories. This yields a formal, modular framework of biform theory graphs which mixes specifications and implementations sharing the module system and typing information. We present automated knowledge management work flows that interface to existing specification/programming tools and enable an OpenMath Machine, that operationalizes biform theories, evaluating expressions by exhaustively applying the implementations of the respective operators. We evaluate the new biform framework by adding implementations to the OpenMath standard content dictionaries.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
