Automated Theorem Proving in Temporal Logic:T-Resolution

被引：0

作者：

招兆铿

戴军

陈文丹

机构：

来源：

Journal of Computer Science and Technology | 1994年 / 01期

关键词：

Temporal logic; automated theorem proving; T-resolution; reasoning; soundness; completeness;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：53 / 62

页数：10

共 7 条

[1] Gallaire H,Minker J,Nicolas J-M.Logic and databases: A deductive approach. ACM Computing Surveys . 1984
[2] Shoham Y.Temporal logics in AI: Semantical and ontological considerations. Artificial Intelligence . 1987
[3] Shoham Y.Reasoning about Change. . 1988
[4] Chang Chin-liang,Richard Char-tung Lee.Symbolic logic and mechanical theorem proving. . 1973
[5] McDermott D,Doyle J.Non-monotonic logic I. Artificial Intelligence . 1980
[6] Allen J F.Maintaining knowledge about temporal intervals. Communications of the ACM . 1983
[7] Dean T,McDermott D.Temporal data base management. Artificial Intelligence . 1987

← 1 →