首页    期刊浏览 2024年09月18日 星期三
登录注册

文章基本信息

  • 标题:On Unification of QBF Resolution-Based Calculi
  • 本地全文:下载
  • 作者:Mikolas Janota ; Leroy Chew ; Olaf Beyersdorff
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2014
  • 卷号:2014
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    Several calculi for quantified Boolean formulas (QBFs) exist, butrelations between them are not yet fully understood.This paper defines a novel calculus, which is resolution-based andenables unification of the principal existing resolution-based QBFcalculi, namely Q-resolution, long-distance Q-resolution and the expansion-basedcalculus Exp+Res. All these calculi play an important role in QBF solving.This paper shows simulation results for the new calculus and some of itsvariants. Further, we demonstrate how to obtain winning strategies for the universalplayer from proofs in the calculus.We believe that this new proof system opens new avenues for furtherresearch and provides a suitable formalism for certification of existing solvers.

国家哲学社会科学文献中心版权所有