Paper detail

Relativisation makes contradictions harder for Resolution

We provide a number of simplified and improved separations between pairs of Resolution-with-bounded-conjunction refutation systems, Res(d), as well as their tree-like versions, Res*(d). The contradictions we use are natural combinatorial principles: the Least number principle, LNP_n and an ordered variant thereof, the Induction principle, IP_n. LNP_n is known to be easy for Resolution. We prove that its relativisation is hard for Resolution, and more generally, the relativisation of LNP_n iterated d times provides a separation between Res(d) and Res(d+1). We prove the same result for the iterated relativisation of IP_n, where the tree-like variant Res*(d) is considered instead of Res(d). We go on to provide separations between the parameterized versions of Res(1) and Res(2). Here we are able again to use the relativisation of the LNP_n, but the classical proof breaks down and we are forced to use an alternative. Finally, we separate the parameterized versions of Res*(1) and Res*(2). Here, the relativisation of IP_n will not work as it is, and so we make a vectorising amendment to it in order to address this shortcoming