Propositional PSPACE reasoning with boolean programs versus quantified Boolean formulas

被引：0
|
作者：
Skelley, A [1 ]
机构：
[1] Univ Toronto, Dept Comp Sci, Toronto, ON M5S 3G4, Canada
来源：
AUTOMATA , LANGUAGES AND PROGRAMMING, PROCEEDINGS | 2004年 / 3142卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a new propositional proof system based on a somewhat recent characterization of polynomial space (PSPACE) called Boolean programs, due to Cook and Soltys. The Boolean programs are like generalized extension atoms, providing a parallel to extended Frege. We show that this new system, BPLK, is polynomially equivalent to the system G, which is based on the familiar but very different quantified Boolean formula (QBF) characterization of PSPACE due to Stockmeyer and Meyer. This equivalence is proved by way of two translations, one of which uses an idea reminiscent of the c-terms of Hilbert and Bernays.
引用
收藏
页码：1163 / 1175
页数：13
相关论文
共 50 条
  • [1] A Structural Approach to Reasoning with Quantified Boolean Formulas
    Pulina, Luca
    Tacchella, Armando
    [J]. 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, : 596 - 602
  • [2] A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving
    Scholl, Christoph
    Jiang, Jie-Hong Roland
    Wimmer, Ralf
    Ge-Ernst, Aile
    [J]. THIRTY-THIRD AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTY-FIRST INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / NINTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2019, : 1584 - 1591
  • [3] Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas
    Egly, Uwe
    Woltran, Stefan
    [J]. COMPUTATIONAL MODELS OF ARGUMENT, 2006, 144 : 133 - 144
  • [4] Boolean functions as models for quantified Boolean formulas
    Buening, Hans Kleine
    Subramani, K.
    Zhao, Xishun
    [J]. JOURNAL OF AUTOMATED REASONING, 2007, 39 (01) : 49 - 75
  • [5] On Boolean models for Quantified Boolean Horn formulas
    Büning, HK
    Subramani, K
    Zhao, XS
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 : 93 - 104
  • [6] Boolean Functions as Models for Quantified Boolean Formulas
    Hans Kleine Büning
    K. Subramani
    Xishun Zhao
    [J]. Journal of Automated Reasoning, 2007, 39 : 49 - 75
  • [7] Solving advanced reasoning tasks using quantified Boolean formulas
    Egly, U
    Eiter, T
    Tompits, H
    Woltran, S
    [J]. SEVENTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-2001) / TWELFTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-2000), 2000, : 417 - 422
  • [8] Reasoning in Abstract Dialectical Frameworks Using Quantified Boolean Formulas
    Diller, Martin
    Wallner, Johannes Peter
    Woltran, Stefan
    [J]. COMPUTATIONAL MODELS OF ARGUMENT, 2014, 266 : 241 - 252
  • [9] Reasoning in abstract dialectical frameworks using quantified Boolean formulas
    Diller, Martin
    Wallner, Johannes Peter
    Woltran, Stefan
    [J]. ARGUMENT & COMPUTATION, 2015, 6 (02) : 149 - 177
  • [10] Symmetries of Quantified Boolean Formulas
    Kauers, Manuel
    Seidl, Martina
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2018, 2018, 10929 : 199 - 216
12345