为自动定理证明器逃向Mizar
计算机科学中的逻辑
2012-05-02 v2
摘要
我们宣布一个将E定理证明器的推导映射到Mizar证明的工具。我们的映射补充了先前从Mizar推理检查问题为自动定理证明器生成问题的工作。我们描述了该工具，解释了映射，并展示了我们如何解决在不同逻辑形式体系之间映射证明时出现的一些困难，即使它们基于相同的逻辑推论概念（即带等词的一阶经典逻辑），如Mizar和E那样。
引用
@article{arxiv.1204.6615,
title = {Escape to Mizar for ATPs},
author = {Jesse Alama},
journal= {arXiv preprint arXiv:1204.6615},
year = {2012}
}
备注
10 pages. Submitted to PAAR 2012 (Practical Aspects of Automated Reasoning, Manchester, June 2012, http://www.eprover.org/EVENTS/PAAR-2012.html)