English

应用科学学报 ›› 1994, Vol. 12 ›› Issue (3): 246-252.

• 论文 • 上一篇    下一篇

自动定理证明中带有等词的连接法

缪淮扣, 吴茂康   

  1. 上海科学技术大学
  • 收稿日期:1992-03-20 修回日期:1992-09-10 出版日期:1994-09-30 发布日期:1994-09-30

THE CONNECTION METHOD WITH EQUALITY FOR AUTOMATED THEOREM PROVING

MIAO HUAIKOU, WU MAOKANG   

  1. Shanghai University of Science and Technology fomerly
  • Received:1992-03-20 Revised:1992-09-10 Online:1994-09-30 Published:1994-09-30

PDF

70

摘要： 连接法是一种较新的自动定理证明的方法.该文讨论了带有等词的连接法,给出了形式化的定义,证明了带有等词的逻辑公式是eq有效的当且仅当它有互补复合例的规范矩阵的定理,并设计了带有等词的连接法的有关算法.

关键词: 连接法, 等词, 自动定理证明, 互补

Abstract: This paper diseusses the connection method with equality in automated theorem proving.The formal definitions are given. The theorem that a logic formula with equality is eq-valid if and only if it has a complementary formal matrix of a compound instance is proved,and several algorithms about the connec-tion method with equality are designed.

Key words: equality, Automated theoren proving, connection method, complementary