Mizar中数学形式化的自动推理与证明呈现支持
人工智能
2011-07-27 v1
摘要
本文介绍了将多种自动推理和证明呈现工具与Mizar系统相结合，用于数学形式化。该组合形成了一个名为MizAR的在线服务，类似于一阶自动推理的SystemOnTPTP服务。与SystemOnTPTP的主要区别在于：MizAR使用面向人类数学家的Mizar语言（而非SystemOnTPTP中使用的纯一阶逻辑），并且该服务建立在大型Mizar数学库（包含先前定理、定义和证明）的背景下（而非SystemOnTPTP中解决的孤立问题）。这些差异为自动推理和证明呈现工具带来了新的挑战和机遇。本文描述了MizAR的整体结构，并介绍了为使其成为有用的数学服务而集成的自动推理系统和证明呈现工具。
引用
@article{arxiv.1005.4592,
title = {Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar},
author = {Josef Urban and Geoff Sutcliffe},
journal= {arXiv preprint arXiv:1005.4592},
year = {2011}
}
备注
To appear in 10th International Conference on. Artificial Intelligence and Symbolic Computation AISC 2010