A decision procedure and complete axiomatization of finite interval temporal logic with projection

被引：37

作者：

Bowman, H ^{[1
]}

Thompson, S ^{[1
]}

机构：

[1] Univ Kent, Canterbury CT2 7NF, Kent, England

来源：

JOURNAL OF LOGIC AND COMPUTATION | 2003年 / 13卷 / 02期

关键词：

tableau; temporal; decision procedure; interval; chop; projection; normal form; complete axiomatization;

D O I：

10.1093/logcom/13.2.195

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents a complete axiomatization for propositional interval temporal logic (PITL) with projection. The axiomatization is based on a tableau decision procedure for the logic, which in turn is founded upon a normal form for PITL formluae, The construction of the axiomatization provides a general mechanism for generating axiomatizations thus: given a normal form for a new connective, axioms can be generated for the connective from the tableau construction using that normal form. The paper concludes with a discussion of aspects of compositionality for PITL with projection.

引用

页码：195 / 239

页数：45

共 29 条

[1]

BARRINGER H, 1989, LECT NOTES ARTIFICIA, V430

[2]

BELL J. L., 1977, COURSE MATH LOGIC

[3]

BENARI M, 1981, 8TH ANN ACM S PRINC, P164

[4]

Bowman H., 1999, Formal Aspects of Computing, V11, P132, DOI 10.1007/s001650050045

[5]

Bowman H, 1998, LECT NOTES ARTIF INT, V1397, P108

[6]

BOWMAN H, 1997, 397 U KENT COMP LAB

[7]

BOWMAN H, 1998, 898 U KENT CANT COMP

[8]

BOWMAN H, 1997, ICTL 97 INT C TEMP L

[9]

CAU A, 1997, 4 AMAST WORKSH REAL, V1231

[10]

Duan ZH., 1996, THESIS U NEWCASTLE T

← 1 2 3 →