Refutation complexity of relativized spectra

22.03.2012 15:00 - 16:30

M. Müller (U Wien)

How difficult is it to prove that a given first-order sentence does not have a finite model of a given size? This can be understood in two natural, roughly equivalent ways. First, as a question for how strong a fragment of arithmetic needs to be to prove the statement. Second, as a question concerning proof lengths in certain propositional calculi. The talk gives a short introduction to proof complexity and presents some exponential lower bounds for the \(R(k)\) systems. This is joint work with Albert Atserias and Sergi Oliva.

Organiser:

KGRC

Location:
SR 101, 2. St., Währinger Str. 25