• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Intelligent computer mathematics >Formal Mathematics on Display: A Wiki for Flyspeck
【24h】

Formal Mathematics on Display: A Wiki for Flyspeck

机译：展示的正规数学：Flyspeck Wiki

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

摘要

The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype Flyspeck Wiki as an instance of Agora for HOL Light formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales's informal Flyspeck book, and the formal Flyspeck development. The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.
机译：Agora系统是原型“ Wiki for Formal Mathematics”，旨在支持在证明助手中开发和记录大型数学形式化。 Agora中实现的功能包括浏览器内编辑，强大的AI / ATP证明建议，验证和HTML渲染。 HTML呈现包含超链接，并提供每个证明步骤的证明状态的按需说明。在本文中，我们将Flyspeck Wiki原型展示为Agora的HOL Light形式化实例。 Wiki可用于数学的形式化和编写有关数学的非正式Wiki页面。这样的非正式页面可能包含正式文本的孤岛，此处用于在Hales的非正式Flyspeck书与正式Flyspeck开发之间提供初始的交叉链接。 Agora平台旨在解决大型形式化项目上的分布式Wiki风格的协作，特别是立即编辑，验证和呈现正式代码方面，以及逐步和相互重构以及初始非正式文本及其形式化的对应方面。在这里，我们在Flyspeck Wiki中突出显示了这些功能。

著录项

  • 来源
    《Intelligent computer mathematics》|2013年|152-167|共16页
  • 会议地点 Bath(GB)
  • 作者

    Carst Tankink; Cezary Kaliszyk; Josef Urban; Herman Geuvers;

  • 作者单位

    ICIS, Radboud Universiteit Nijmegen, Netherlands;

    Institut fuer Informatik, Universitaet Innsbruck, Austria;

    ICIS, Radboud Universiteit Nijmegen, Netherlands;

    ICIS, Radboud Universiteit Nijmegen, Netherlands,Technical University Eindhoven, Netherlands;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号