The power of the ''always'' operator in first-order temporal logic

被引：2

作者：

Kaminski, M ^{[1
]}

Wong, CK ^{[1
]}

机构：

[1] UNIV TEXAS, DEPT COMP SCI, AUSTIN, TX 78712 USA

来源：

THEORETICAL COMPUTER SCIENCE | 1996年 / 160卷 / 1-2期

关键词：

D O I：

10.1016/0304-3975(95)00108-5

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

It is shown that in first-order linear-time temporal logic, validity questions can be translated into validity questions of formulas not containing ''next'' or ''until'' operators. The translation can be performed in linear time.

引用

页码：271 / 281

页数：11

共 50 条

[1] Policy Monitoring in First-Order Temporal Logic
Basin, David
Klaedtke, Felix
Mueller, Samuel
[J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 1 - 18
[2] First-order temporal logic monitoring with BDDs
Klaus Havelund
Doron Peled
Dogan Ulus
[J]. Formal Methods in System Design, 2020, 56 : 1 - 21
[3] Nonclausal deduction in first-order temporal logic
[J]. Abadi, Martin, 1600, (37):
[4] First-order temporal logic monitoring with BDDs
Havelund, Klaus
Peled, Doron
Ulus, Dogan
[J]. FORMAL METHODS IN SYSTEM DESIGN, 2020, 56 (1-3) : 1 - 21
[5] Equality and monodic first-order temporal logic
Degtyarev A.
Fisher M.
Lisitsa A.
[J]. Studia Logica, 2002, 72 (2) : 147 - 156
[6] Proof planning for first-order temporal logic
Castellini, C
Smaill, A
[J]. AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 235 - 249
[7] First-order logic with two variables and unary temporal logic
Etessami, K
Vardi, MY
Wilke, T
[J]. INFORMATION AND COMPUTATION, 2002, 179 (02) : 279 - 295
[8] First-order logic with two variables and unary temporal logic
Etessami, K
Vardi, MY
Wilke, T
[J]. 12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1997, : 228 - 235
[9] THE FIRST-ORDER LOGIC OF CZF IS INTUITIONISTIC FIRST-ORDER LOGIC
Passmann, Robert
[J]. JOURNAL OF SYMBOLIC LOGIC, 2024, 89 (01) : 308 - 330
[10] First-Order Logic and First-Order Functions
Freire, Rodrigo A.
[J]. LOGICA UNIVERSALIS, 2015, 9 (03) : 281 - 329

← 1 2 3 4 5 →