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).