SIMPLE INTERPRETATIONS AMONG COMPLICATED THEORIES

被引：5

作者：

GRADEL, E ^{[1
]}

机构：

[1] UNIV PISA,I-56100 PISA,ITALY

来源：

INFORMATION PROCESSING LETTERS | 1990年 / 35卷 / 05期

关键词：

complexity; Decision problem for mathematical theories; interpretations; temporal logic;

D O I：

10.1016/0020-0190(90)90051-X

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We show that several mathematical theories whose decision problems are solvable but not elementary recursive can be interpreted into quantified propositional temporal logic (QPTL) by interpretations which do not increase the number of quantifier alternations. Using complexity results for QPTL due to Sistla, Vardi and Wolper we infer (k-1)-fold exponential space upper bounds for the formulae of these theories with at most k quantifier alternations. Thus, temporal logic, besides being a convenient tool for reasoning about programs, provides in an elegant way complexity results for other mathematical theories. © 1990.

引用

页码：235 / 238

页数：4