White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Proof Complexity of Modal Resolution Systems

Sigley, Sarah Elizabeth (2019) Proof Complexity of Modal Resolution Systems. PhD thesis, University of Leeds.

Sigley_SE_Computing_PhD_2019.pdf - Final eThesis - complete (pdf)
Available under License Creative Commons Attribution-Noncommercial-Share Alike 2.0 UK: England & Wales.

Download (1062Kb) | Preview


In this thesis we initiate the study of the proof complexity of modal resolution systems. To our knowledge there is no previous work on the proof complexity of such systems. This is in sharp contrast to the situation for propositional logic where resolution is the most studied proof system, in part due to its close links with satisfiability solving. We focus primarily on the proof complexity of two recently proposed modal resolution systems of Nalon, Hustadt and Dixon, one of which forms the basis of an existing modal theorem prover. We begin by showing that not only are these two proof systems equivalent in terms of their proof complexity, they are also equivalent to a number of natural refinements. We further compare the proof complexity of these systems with an older, more complicated modal resolution system of Enjalbert and Farinas del Cerro, showing that this older system p-simulates the more streamlined calculi. We then investigate lower bound techniques for modal resolution. Here we see that whilst some propositional lower bound techniques (i.e. feasible interpolation) can be lifted to the modal setting with only minor modifications, other propositional techniques (i.e. size-width) fail completely. We further develop a new lower bound technique for modal resolution using Prover-Delayer games. This technique can be used to establish "genuine" modal lower bounds (i.e lower bounds on the number of modal inferences) for the size of tree-like modal resolution proofs. We apply this technique to a new family of modal formulas, called the modal pigeonhole principle to demonstrate that these formulas require exponential size modal resolution proofs. Finally we compare the proof complexity of tree-like modal resolution systems with that of modal Frege systems, using our modal pigeonhole principle to obtain a "genuinely" modal separation between them.

Item Type: Thesis (PhD)
Keywords: modal logic, resolution, proof complexity
Academic Units: The University of Leeds > Faculty of Engineering (Leeds) > School of Computing (Leeds)
Identification Number/EthosID: uk.bl.ethos.798002
Depositing User: Miss Sarah Elizabeth Sigley
Date Deposited: 30 Jan 2020 12:07
Last Modified: 11 Mar 2020 10:54
URI: http://etheses.whiterose.ac.uk/id/eprint/25782

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)