使用 auto2 在无类型集合论中形式化基本群
计算机科学中的逻辑
2017-10-03 v1
摘要
我们提出了一个使用 auto2 在无类型集合论中形式化数学的新框架。使用该框架，我们在 Isabelle/FOL 中形式化了从集合论公理到任意拓扑空间的基本群定义的整个发展链。auto2 证明器被用作唯一的自动化工具，并在整个项目中实现了简洁的证明脚本。
引用
@article{arxiv.1707.04757,
title = {Formalization of the fundamental group in untyped set theory using auto2},
author = {Bohua Zhan},
journal= {arXiv preprint arXiv:1707.04757},
year = {2017}
}
备注
17 pages, accepted for ITP 2017