We use cookies to improve your experience with our site.
Zhao Zhaokeng, Dai Jun, Chen Wendan. Automated Theorem Proving in Temporal Logic:T-Resolution[J]. Journal of Computer Science and Technology, 1994, 9(1): 53-62.
Citation: Zhao Zhaokeng, Dai Jun, Chen Wendan. Automated Theorem Proving in Temporal Logic:T-Resolution[J]. Journal of Computer Science and Technology, 1994, 9(1): 53-62.

Automated Theorem Proving in Temporal Logic:T-Resolution

  • This paper presentes a novel resolution method, T-resolution, based on the first order temporal logic. The primary claim of this method is its soundness and completeness. For this purpose, we construct the corresponding semantic trees and extend Herbrand's Theorem.
  • loading

Catalog

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return