摘要
连接法是一种较新的自动定理证明的方法．该文讨论了带有等词的连接法，给出了形式化的定义，证明了带有等词的逻辑公式是ｅｑ有效的当且仅当它有互补复合例的规范矩阵的定理，并设计了带有等词的连接法的有关算法．
This paper diseusses the connection method with equality in automatedtheorem proving.The formal definitions are given. The theorem that a logicformula with equality is eq-valid if and only if it has a complementary formalmatrix of a compound instance is proved,and several algorithms about the connec-tion method with equality are designed.
出处
《应用科学学报》
CAS
CSCD
1994年第3期246-252,共7页
Journal of Applied Sciences
关键词
自动定理证明
连接法
等词
Automated theoren proving, connection method, equality,complementary.
