Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Relativisation Provides Natural Separations for Resolution-Based Proof Systems
verfasst von : Stefan Dantchev
Erschienen in: Computer Science – Theory and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We prove a number of simplified and improved separations between pairs of Resolution with bounded conjunction proof systems, Res(
d
) , as well as their tree-like versions, Res* (
d
). The tautologies, which we use, are natural combinatorial principles: the Least Number Principle (
LNP
n
) and a variant of 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 natural separation between Res(
d
) and Res(
d
+1). We prove the same result for the iterated relativisation of
IP
n
if the tree-like proof system Res*(
d
) is considered instead of Res (
d
).