Moritz Müller
On lower bounds for Res(k)
Kurt Gödel Research Center for Mathematical Logic (KGRC), Vienna
| DATE: | Tuesday, January 10, 2012 |
ABSTRACT
A first-order sentence without finite models straightforwardly translates to a sequence of propositional contradictions. If the sentence has an infinite model, Riis' Gap Theorem gives an exponential lower bound on the length of its treelike Resolution proofs. For relativized such sentences Dantchev and Riis establish an exponential lower bound even in daglike Resolution (and treelike Res(k) for each fixed k). For a different translation intopropositional logic we establish exponential lower bounds for dag like Res(k) (for each fixed k).
Tuesday, January 10, 2012, 4:00 pm – 5:00 pm, Seminar room Zemanek
(Favoritenstrasse 9-11, ground floor)
