• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Intelligent computer mathematics >A Universal Machine for Biform Theory Graphs
【24h】

A Universal Machine for Biform Theory Graphs

机译：双重理论图的通用机器

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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 Mmt/ 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.
机译：广义上讲，存在两种用于数学的语义感知助手系统：证明助手在逻辑上表达语义并强调演绎，计算机代数系统在编程语言中表达语义并强调计算。在一段时间内，将两种方法的互补优势相结合，同时弥补其互补劣势已成为机械化数学界的重要目标。我们采用双重理论的思想，并在Mmt / OMDoc框架中对其进行了解释，该框架引入了“基础理论”方法，因此可以将逻辑和编程语言都表示为理论。这产生了一个双形式理论图的形式化，模块化框架，该框架混合了规范和实现，共享模块系统并键入信息。我们提出了自动化的知识管理工作流程，该流程与现有的规范/编程工具相接，并启用OpenMath机器，该机器可操作双重理论，并通过详尽地应用各个运算符的实现来评估表达式。我们通过将实现添加到OpenMath标准内容字典中来评估新的双形式框架。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号