| Automated Theorem Proving in Temporal Logic:T-Resolution |
| |
| 作者姓名： | Zhao Zhaokeng Dai Jun Chen Wendan |
| |
| 作者单位： | [1]DepartmentofComputerScience,FudanUniversity,Shanghai200433 [2]DepartmentofComputerScience,FudanUniversit |
| |
| 摘 要： | 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.
|
| 关 键 词： | 人工智能 时序逻辑 T－分辨力 |
Automated theorem proving in temporal logic: T-resolution |
| |
| 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. |
| |
| Authors: | Zhaokeng Zhao Jun Dai Wendan Chen |
| |
| Affiliation: | Department of Computer Science; Fudan Universitg; Shanghai 200433; |
| |
| 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. |
| |
| Keywords: | Temporal logic automated theorem proving T-resolution reasoning soundness completeness |
| 本文献已被 CNKI 维普 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
