J4

• 计算机科学 • Previous Articles     Next Articles

Hyper Tableau with Equality

FENG Sha-sha1,2, SUN Ji-gui1,2, WU Xia1   

  1. 1. College of Computer Science and Technology, Jilin University, Changchun 130012, China;2. Key Laboratory of Symbolic Computation and Knowledge Engineer of Ministry of Education, Jilin University, Changchun 130012, China
  • Received:2004-12-13 Revised:1900-01-01 Online:2005-07-26
  • Contact: SUN Ji-gui

Abstract: The hyper tableau calculus is capable of solving first -order logic problems with equality by introducing superposition to it, which i s competent in equality reasoning. The new tableau calculus is backtrack-free a s well as complete. It is an attempt at completing the machine proving of the fi rst-order logic theorem with equality via the tableau calculus.

Key words: hyper tableau calculus, superposition method, equality

CLC Number: 

  • TP31