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). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover-Delayer games, which can be used to establish "genuine" modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrubeš (Ann Pure Appl Log 157(2-3):194-205, 2009) and obtain a "genuinely" modal separation.