J4

• 数学 • Previous Articles     Next Articles

Relational Extension Rule

WU Xia1,2, YU Haihong1,2, LI Zehai3, LI He1,2, SUN Jiayu4   

  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; 3. Shanghai Futures Exchange R & D Center, Shanghai 200122, China;4. School of Mathematics and Statistics, Northeast Normal University, Changchun 130024, China
  • Received:2007-07-31 Revised:1900-01-01 Online:2008-05-26 Published:2008-05-26
  • Contact: WU Xia

Abstract: The modal logics was translated into a firstorder fragment by relational encoding method at first. And then we used the firstorder extension rule prover to deal with the fragment. Namely, we presented a new reas oning method for modal logics. The proof of its soundness and completeness was given at last.

Key words: theorem proving, modal logic, extension rule, relational translation

CLC Number: 

  • TP31