• Articles • Previous Articles     Next Articles

Automated Theorem Proving in Temporal Logic:T-Resolution

Zhao Zhaokeng; Dai Jun; Chen Wendan;   

  1. Department of Computer Science; Fudan Universitg; Shanghai 200433;
  • Online:1994-01-10 Published:1994-01-10

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.

Key words: similarity; relevancy; Hownet; question-answering; natural language processing;

[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. ……….
[1] Sheng-Luan Hou, Xi-Kun Huang, Chao-Qun Fei, Shu-Han Zhang, Yang-Yang Li, Qi-Lin Sun, Chuan-Qing Wang. A Survey of Text Summarization Approaches Based on Deep Learning [J]. Journal of Computer Science and Technology, 2021, 36(3): 633-663.
[2] Peng Ni, Su-Yun Zhao, Zhi-Gang Dai, Hong Chen, Cui-Ping Li. Partial Label Learning via Conditional-Label-Aware Disambiguation [J]. Journal of Computer Science and Technology, 2021, 36(3): 590-605.
[3] Lian-Lian Wu, Yu-Qi Wen, Xiao-Xi Yang, Bo-Wei Yan, Song He, Xiao-Chen Bo. Synthetic Lethal Interactions Prediction Based on Multiple Similarity Measures Fusion [J]. Journal of Computer Science and Technology, 2021, 36(2): 261-275.
[4] Zhi-Xing Li, Yue Yu, Tao Wang, Gang Yin, Xin-Jun Mao, Huai-Min Wang. Detecting Duplicate Contributions in Pull-based Model Combining Textual and Change Similarities [J]. Journal of Computer Science and Technology, 2021, 36(1): 191-206.
[5] Yuan Huang, Nan Jia, Hao-Jie Zhou, Xiang-Ping Chen, Zi-Bin Zheng, Ming-Dong Tang. Learning Human-Written Commit Messages to Document Code Changes [J]. Journal of Computer Science and Technology, 2020, 35(6): 1258-1277.
[6] Xiang-Guang Zhou, Ren-Bin Gong, Fu-Geng Shi, Zhe-Feng Wang. PetroKG: Construction and Application of Knowledge Graph in Upstream Area of PetroChina [J]. Journal of Computer Science and Technology, 2020, 35(2): 368-378.
[7] Jun-Hua Fang, Peng-Peng Zhao, An Liu, Zhi-Xu Li, Lei Zhao. Scalable and Adaptive Joins for Trajectory Data in Distributed Stream System [J]. Journal of Computer Science and Technology, 2019, 34(4): 747-761.
[8] Jinoh Kim, Alex Sim. A New Approach to Multivariate Network Traffic Analysis [J]. Journal of Computer Science and Technology, 2019, 34(2): 388-402.
[9] Li Li, Tegawendé F. Bissyandé, Hao-Yu Wang, Jacques Klein. On Identifying and Explaining Similarities in Android Apps [J]. Journal of Computer Science and Technology, 2019, 34(2): 437-455.
[10] Sai-Sai Gong, Wei Hu, Wei-Yi Ge, Yu-Zhong Qu. Modeling Topic-Based Human Expertise for Crowd Entity Resolution [J]. Journal of Computer Science and Technology, 2018, 33(6): 1204-1218.
[11] Guo-Wei Wang, Jin-Dou Zhang, Jing Li. Complete Your Mobility: Linking Trajectories Across Heterogeneous Mobility Data Sources [J]. , 2018, 33(4): 792-806.
[12] Jun-Li Zhao, Zhong-Ke Wu, Zhen-Kuan Pan, Fu-Qing Duan, Jin-Hua Li, Zhi-Han Lv, Kang Wang, Yu-Cong Chen. 3D Face Similarity Measure by Fréchet Distances of Geodesics [J]. , 2018, 33(1): 207-222.
[13] Rong Wang, Tian-Lei Hu, Gang Chen. Where Do Local Experts Go? Evaluating User Geo-Topical Similarity for Top-N Place Recommendation [J]. , 2018, 33(1): 190-206.
[14] Yi-Li Fang, Hai-Long Sun, Peng-Peng Chen, Ting Deng. Improving the Quality of Crowdsourced Image Labeling via Label Similarity [J]. , 2017, 32(5): 877-889.
[15] Meng Chen, Xiaohui Yu, Yang Liu. Mining Object Similarity for Predicting Next Locations [J]. , 2016, 31(4): 649-660.
Full text



[1] Xie Li; Chen Peipei; Yang Peigen; Sun Zhongxiu;. The Design and Implementation of an OA System ZGL1[J]. , 1988, 3(1): 75 -80 .
[2] Xu Zhiming;. Discrete Interpolation Surface[J]. , 1990, 5(4): 329 -332 .
[3] Zhang Bo; Zhang Ling;. A Relation Matrix Approach to Labelling Temporal Relations in Scheduling[J]. , 1991, 6(4): 339 -346 .
[4] Shen Yidong;. Form alizing Incomplete Knowledge in Incomplete Databases[J]. , 1992, 7(4): 295 -304 .
[5] Zhang Bo; Zhang Ling;. On Memory Capacity of the Probabilistic Logic Neuron Network[J]. , 1993, 8(3): 62 -66 .
[6] Shuai Dianxun;. Concurrent Competitive Wave Approach to Hyper-Distributed Hyper-Parallel AI Processing[J]. , 1997, 12(6): 543 -554 .
[7] CHEN Yisong(陈毅松),LU Jian(卢坚),SUN Zhengxing(孙正兴)and ZHANG Fuyan(张福炎). Greylevel Difference Classification Algorithm in Fractal Image Compression[J]. , 2002, 17(2): 0 .
[8] I-Shyan Hwang, I-Feng Huang, and Shin-Cheng Yu. Dynamic Fuzzy Controlled RWA Algorithm for IP/GMPLS over WDM Networks[J]. , 2005, 20(5): 717 -727 .
[9] Hua Li, Shui-Cheng Yan, and Li-Zhong Peng[1]. Robust Non-Frontal Face Alignment with Edge Based Texture[J]. , 2005, 20(6): 849 -854 .
[10] Zhong-Xuan Liu, Shi-Guo Lian, and Zhen Ren. Quaternion Diffusion for Color Image Filtering[J]. , 2006, 21(1): 126 -136 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved