Complexity of Presburger arithmetic with fixed quantifier dimension

被引：18
|
作者：
Schöning U. [1 ]
机构：
[1] Abt. Theoretische Informatik, Universität Ulm
来源：
Theory of Computing Systems | 1997年 / 30卷 / 4期
关键词：
Decision Problem; Boolean Variable; Logical Theory; Universal Quantifier; Chinese Remainder Theorem;
D O I：
10.1007/BF02679468
中图分类号：
学科分类号：
摘要：
It is shown that the decision problem for formulas in Presburger arithmetic with quantifier prefix [∃1∀2 ⋯ ∃m∀3] (for m odd) and [∃1∀2 ⋯ ∀m∃3] (for m even) is complete for the class ΣPm of the polynomial-time hierarchy. Furthermore, the prefix type [∃∀∃∃] is complete for ΣP2, and the prefix type [∃∀] is complete for NP. This improves results (and solves a problem left open) by Grädel [7].
引用
收藏
页码：423 / 428
页数：5
相关论文
共 50 条
  • [1] Complexity of Presburger arithmetic with fixed quantifier dimension
    Abt. Theoretische Informatik, Universität Ulm, D-89069 Ulm, Germany
    Theory Comput. Syst., 4 (423-428):
  • [2] Complexity of Presburger arithmetic with fixed quantifier dimension
    Schoning, U
    THEORY OF COMPUTING SYSTEMS, 1997, 30 (04) : 423 - 428
  • [3] THE COMPLEXITY OF PRESBURGER ARITHMETIC WITH BOUNDED QUANTIFIER ALTERNATION DEPTH
    FURER, M
    THEORETICAL COMPUTER SCIENCE, 1982, 18 (01) : 105 - 111
  • [4] Parametric Presburger arithmetic: complexity of counting and quantifier elimination
    Bogart, Tristram
    Goodrick, John
    Nguyen, Danny
    Woods, Kevin
    MATHEMATICAL LOGIC QUARTERLY, 2019, 65 (02) : 237 - 250
  • [5] Verifying and reflecting quantifier elimination for Presburger arithmetic
    Chaieb, A
    Nipkow, T
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 367 - 380
  • [6] Quantifier elimination for counting extensions of Presburger arithmetic
    Chistikov, Dmitry
    Haase, Christoph
    Mansutti, Alessio
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2022), 2022, 13242 : 225 - 243
  • [7] Interpolating Quantifier-Free Presburger Arithmetic
    Kroening, Daniel
    Leroux, Jerome
    Ruemmer, Philipp
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2010, 6397 : 489 - +
  • [8] Effective Quantifier Elimination for Presburger Arithmetic with Infinity
    Lasaruk, Aless
    Sturm, Thomas
    COMPUTER ALGEBRA IN SCIENTIFIC COMPUTING, PROCEEDINGS, 2009, 5743 : 195 - +
  • [9] Complexity of Short Presburger Arithmetic
    Danny Nguyen
    Pak, Igor
    STOC'17: PROCEEDINGS OF THE 49TH ANNUAL ACM SIGACT SYMPOSIUM ON THEORY OF COMPUTING, 2017, : 812 - 820
  • [10] Generic Complexity of Presburger Arithmetic
    Alexander N. Rybalov
    Theory of Computing Systems, 2010, 46 : 2 - 8
12345