摘要翻译：
本文将几种自动推理和证明工具与数学形式化的Mizar系统相结合。这种组合形成了一个名为MizAR的在线服务，类似于用于一阶自动推理的SystemOnTPTP服务。与SystemOnTPTP的主要区别在于使用面向人类数学家的Mizar语言（而不是SystemOnTPTP中使用的纯一阶逻辑），并在包含先前定理、定义和证明的大型Mizar数学库的上下文中设置服务（而不是SystemOnTPTP中解决的孤立问题）。这些差异为自动推理和证明表示工具提出了新的挑战和新的机会。本文描述了MizAR的总体结构，并给出了自动推理系统和证明表示工具的组合，使MizAR成为一个有用的数学服务。
---
英文标题：
《Automated Reasoning and Presentation Support for Formalizing Mathematics
  in Mizar》
---
作者：
Josef Urban and Geoff Sutcliffe
---
最新提交年份：
2010
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  This paper presents a combination of several automated reasoning and proof presentation tools with the Mizar system for formalization of mathematics. The combination forms an online service called MizAR, similar to the SystemOnTPTP service for first-order automated reasoning. The main differences to SystemOnTPTP are the use of the Mizar language that is oriented towards human mathematicians (rather than the pure first-order logic used in SystemOnTPTP), and setting the service in the context of the large Mizar Mathematical Library of previous theorems,definitions, and proofs (rather than the isolated problems that are solved in SystemOnTPTP). These differences poses new challenges and new opportunities for automated reasoning and for proof presentation tools. This paper describes the overall structure of MizAR, and presents the automated reasoning systems and proof presentation tools that are combined to make MizAR a useful mathematical service.
---
PDF链接：
https://arxiv.org/pdf/1005.4592