Simple interpretations among complicated theories

DOI10.1016/0020-0190(90)90051-XMaRDI QIDQ923068zbMATH OpenFDO

Authors Erich Grädel

Publication date 1990

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(90)90051-X

zbMATH Keywords

complexity of quantifier bounded fragmentsdecision complexityexistential monadic second order theory of finite linear ordersexponential upper bounds of space complexityextensions of Presburger arithmeticfirst order theories of m-ary trees with m successorsformal theoriesnumber of quantifier alternationsquantified propositional temporal logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Modal logic (including the logic of norms) (03B45) Complexity of computation (including implicit computational complexity) (03D15) Analysis of algorithms and problem complexity (68Q25)

Review text

Let QPTL denote the quantified propositional temporal logic with temporal operators ``nexttime and ``from now on forever and with the time structure of the type of natural numbers. Interpretations of some formal theories in QPTL are described which do not increase the number of quantifier alternations. By use of results of Sistla, Vardi and Wolper on complexity of quantifier bounded fragments of QPTL it gives (k-1)-fold exponential upper bounds of space complexity for the formulae of these theories with at most k quantifier alternations. The theories considered are 1): extensions of Presburger arithmetic by the predicate \(x/_ my\) which expresses that x is a power of m which divides y (for fixed m), 2) first order theories of m-ary trees with m successors, the prefix relation and the equal length relation, 3) the existential monadic second order theory of finite linear orders.

Recommendations

• scientific article; zbMATH DE number 1136071
• The complexity of propositional linear temporal logics
• On the expressivity and complexity of quantitative branching-time temporal logics
• scientific article; zbMATH DE number 2084388
• Temporal logics over linear time domains are in PSPACE

Cites work

• A uniform method for proving lower bounds on the computational complexity of logical theories
• scientific article; zbMATH DE number 3562520 (Why is no real title available?)
• The complementation problem for Büchi automata with applications to temporal logic
• The complexity of propositional linear temporal logics

Cited in

(3)

• Simple theories
• An example of a new simple theory
• Simple sentences that are hard to decide

This page was built for publication: Simple interpretations among complicated theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q923068)