We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 9 Issue 1
January  1994
Turn off MathJax
Article Contents
Abstract
References
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.
shu

Automated Theorem Proving in Temporal Logic:T-Resolution

  • Department of Computer Science; Fudan Universitg; Shanghai 200433;

More Information
  • Published Date: January 09, 1994
    Abstract
  • 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.
    • FullText(HTML)
    • References (3)
  • [1]
    Chang Chin-Bang, Richard Char-tung Lee. Symbolic logic and mechanical theorem proving. Academic Press. 1973.
    [2]
    Abadi M, Manna Z. A timely resolution. Symposium on Logic in Computer Science. 1986,176-186.
    [3]
    Allen J F. Maintaining knowledge about temporal intervals. Communication of ACM, 1983, 26:832-843. ……….
    • Relative Articles
  • Supplements (0)

Catalog

    Get Citation
    PDF
    XML
    Article views (14) PDF downloads (1404) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return