Automated reasoning about elementary point-set topology
Automated reasoning about elementary point-set topology
复制标题
基本点集拓扑的自动推理
DOI：
--
复制
发表时间：
1989
期刊：
影响因子：
--
通讯作者：
W. McCune
中科院分区：
文献类型：
--
作者：
Cynthia A. Wick;W. McCune
在本文中，我们提出了基本点集拓扑的一阶公式，试图扩大可用于自动定理证明程序探索的数学范围。我们目前的拓扑定义和样本引理都在一阶逻辑和子句的形式。然后，我们说明了一些困难，这些样本引理通过一个基本引理的证明，在五个部分。
In this paper we present first-order formulas for basic point-set topology, in an attempt to extend the mathematical range available for exploration with automated theorem-proving programs. We present topology definitions and sample lemmas both in first-order logic and in clausal form. We then illustrate some of the difficulties of these sample lemmas through a proof of a basic lemma in five parts.