使用定理证明器ANDP简化构造几何公理系统

摘要：

ｖｏｎ Ｐｌａｔｏ使用不同的概念对构造几何公理化。他使用１４个公理去刻划构造几何。在这篇文章里研究人员报告了如下事实：一个更短而且更直观的公式能等价替换ｖｏｎ Ｐｌａｔｏ的关于相离和相交的相等相容性第三公理。这个结果是使用定理证明器ＡＮＤＰ做大量的计算机试验后得到的。

关键词： 自动定理证明 构造几何 直觉逻辑

作者: 李大法

作者单位: 大学应用数学系(北京)

会议类型: 国内会议

会议名称: 第五届中国人工智能联合学术会议

会议地点: 西安

会议语种:中文

页码: 39～44

在线出版日期: 1998-10-01（万方平台首次上网日期，不代表论文的发表时间）