Relativization 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. LNPn is known to be easy for Resolution. We prove that its relativization is hard for Resolution, and more generally, the relativization of LNPn iterated d times provides a separation between Res(d) and Res(d+ 1). We prove the same result for the iterated relativization 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(l) and Res(2). Here we are able again to use the relativization 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 relativization of IP_n will not work as it is, and so we make a vectorizing amendment to it in order to address this shortcoming.