首页    期刊浏览 2025年02月26日 星期三
登录注册

文章基本信息

  • 标题:Dependency Schemes in QBF Calculi:Semantics and Soundness
  • 本地全文:下载
  • 作者:Olaf Beyersdorff ; Joshua Blinkhorn
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2016
  • 卷号:2016
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    We study the parametrisation of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on `exhibition' by QBF models, and use it to express a property of dependency schemes called `full exhibition' that is known to be sufficient for soundness in Q-resolution. Introducing a generalised form of the long-distance resolution rule, we propose a complete parametrisation of classical long-distance Q-resolution, and show that full exhibition remains sufficient for soundness. We demonstrate that our approach applies to the current research frontiers by proving that the reflexive resolution path dependency scheme is fully exhibited.

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