NONCLAUSAL DEDUCTION IN 1ST-ORDER TEMPORAL LOGIC

被引：24

作者：

ABADI, M

MANNA, Z

机构：

[1] STANFORD UNIV,DEPT COMP SCI,STANFORD,CA 94305

[2] WEIZMANN INST SCI,IL-76100 REHOVOT,ISRAEL

来源：

JOURNAL OF THE ACM | 1990年 / 37卷 / 02期

关键词：

D O I：

10.1145/77600.77617

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper presents a proof system for first-order temporal logic. The system extends the nonclausal resolution method for ordinary first-order logic with equality, to handle quantifiers and temporal operators. Soundness and completeness issues are considered. The use of the system for verifying concurrent programs is discussed and variants of the system for other modal logics are also described. © 1990, ACM. All rights reserved.

引用

页码：279 / 317

页数：39

共 42 条

[1]

ABADI M, 1986, LECT NOTES COMPUT SC, V230, P172

[2] THE POWER OF TEMPORAL PROOFS [J].

ABADI, M .

THEORETICAL COMPUTER SCIENCE, 1989, 65 (01) :35-83

[3] TEMPORAL LOGIC PROGRAMMING [J].

ABADI, M ;

MANNA, Z .

JOURNAL OF SYMBOLIC COMPUTATION, 1989, 8 (03) :277-295

[4]

ABADI M, 1986, 1ST ANN S LOG COMP S, P176

[5]

ABADI M, 1985, LECTURE NOTES COMPUT, V193, P1

[6]

ABADI M, 1987, THESIS STANFORD U CA

[7]

CASLEY R, 1986, STANCS861109 STANF U

[8]

CAVALLI A, 1984, 7TH P INT C AUT DED, V170, P113

[9]

CAVALLI A, 1984, JUN ACM SIGCOMM 84 S, P100

[10]

Cresswell M., 1968, INTRO MODAL LOGIC

← 1 2 3 4 5 →