Simple interpretations among complicated theories
type: Item
instance of: scholarly article
title: Simple interpretations among complicated theories
zbMATH Open document ID: 0712.03006
DOI: 10.1016/0020-0190(90)90051-X
author: Erich Grädel
published in: Information Processing Letters
publication date: 1990-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 68Q25
zbMATH DE Number: 4170864
zbMATH Keywords: decision complexity
zbMATH Keywords: quantified propositional temporal logic
zbMATH Keywords: formal theories
zbMATH Keywords: number of quantifier alternations
zbMATH Keywords: complexity of quantifier bounded fragments
zbMATH Keywords: exponential upper bounds of space complexity
zbMATH Keywords: extensions of Presburger arithmetic
zbMATH Keywords: first order theories of m-ary trees with m successors
zbMATH Keywords: existential monadic second order theory of finite linear orders
MaRDI profile type: Publication
cites work: A uniform method for proving lower bounds on the computational complexity of logical theories
cites work: Q4134970
cites work: The complexity of propositional linear temporal logics
cites work: The complementation problem for Büchi automata with applications to temporal logic
description: scientific article; zbMATH DE number 4170864