A game characterisation of tree-like Q-Resolution size

作者：

Highlights：

• Game characterisation for proof size in tree-like Q-Resolution and QU-Resolution.

• One of the first transfers of a propositional lower bound technique to QBF.

• Several applications for the new lower-bound technique.

摘要

•Game characterisation for proof size in tree-like Q-Resolution and QU-Resolution.•One of the first transfers of a propositional lower bound technique to QBF.•Several applications for the new lower-bound technique.

论文关键词：Proof complexity,Resolution,Prover–Delayer games,QBF

论文评审过程：Received 25 June 2015, Revised 6 October 2016, Accepted 27 November 2016, Available online 2 January 2017, Version of Record 6 June 2019.

论文官网地址：https://doi.org/10.1016/j.jcss.2016.11.011