Proof Complexity of Modal Resolution.

We investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3-4):117-134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods-24th international conference, (TABLEAUX'15), pp 185-200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI'17), pp 4919-4923, 2017).

Building Strategies into QBF Proofs.

Strategy extraction is of great importance for quantified Boolean formulas (QBF), both in solving and proof complexity. So far in the QBF literature, strategy extraction has been algorithmically performed proofs. Here we devise the first QBF system where (partial) strategies are built the proof and are piecewise constructed by simple operations along with the derivation.

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF.

Dependency quantified Boolean formulas (DQBF) and QBF dependency schemes have been treated separately in the literature, even though both treatments extend QBF by replacing the linear order of the quantifier prefix with a partial order. We propose to merge the two, by reinterpreting a dependency scheme as a mapping from QBF into DQBF. Our approach offers a fresh insight on the nature of soundness in proof systems for QBF with dependency schemes, in which a natural property called 'full exhibition' is central.