Journal of Applied Sciences ›› 1994, Vol. 12 ›› Issue (3): 246-252.

• Articles • Previous Articles     Next Articles

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

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