Prague-Vienna workshop on Proof Theory and Proof Complexity, 2006

Schedule Prague Vienna Workshop 2006

Wednesday 11-1-2006 Thursday 12-1-2006
10:00-10:40 Pavel Pudlák 10:00-10:40 Mathias Baaz
10:40-11:20 Joost J. Joosten 10:40-11:20 Arnold Beckmann
11:20-11:35 Tea and Coffee
11:20-11:35 Tea and Coffee
11:35-12:15 Markus Latte 11:35-12:15 Rosalie Iemhoff
12:15-14:00  Lunch
12:15-14:00  Lunch
14:00-14:40 Alan Skelley 14:00-14:40 Petr Hájek
14:40-15:20 Marta Bilkova  14:40-15:20 George Metcalfe
15:20-15:40 Tea and Coffee 15:20-15:40 Tea and Coffee
15:40-16:20 Vitezslav Svejdar 15:40-16:20 Evan Goris
16:20-17:00 Pavel Hrubes 16:20-17:00 Jan Krajicek

COORDINATES are as follows. The workshop takes place at Zitna 25 on Wednesday January 11 and Thursday January 12. The conference room shall be indicated with signs to find it. If you are at Zitna 25, there is big door which looks like a little "archway". You can recognize this by the flowershop on the lefthand side. You go through the archway across the courtyard and the institute is through the glass doors at the end.
To find your way around in Prague it is very good to use

SOCIAL EVENTS will comprise a dinner party and possibly something else. The dinner party will be on thursday January 12 at Pivovarsky Dum starting at 18:30. We are thinking of ordering a GOOSE for dinner. Those who want to participate in the goose should contact Joost J. Joosten (jjoosten "include here at" know asap, as the goose has to be ordered and specially prepared in advance.

Wednesday 11-1-2006

10:00-10:40 Speaker: Pavel Pudlák; Title: On search problems and \forall\Sigma_1^b theorems of bounded arithmetic

Abstract: \forall\Sigma_1^b theorems can be viewed as total search problems (total = every instance is solvable). Search problems have been studied in computational complexity theory and the corresponding theorems in bounded arithmetic. The problems of characterizing such consequences of bounded arithmetic and proving that they form an increasing hierarchy are among the most interesting open problems in bounded arithmetic. Solving these problems may help us also classify (exponential) algorithms for solving search problems.

I shall discuss some attempts to solve these two problems.

10:40-11:20 Speaker: Joost J. Joosten; Title: Large objects in modal logics

Abstract: The main topic of this talk will be on things related to lower bounds for PSPACE complete modal logics. Together with Pavel Hrubes and Pavel Pudlák we have had some brainstorm session over the last two months. I shall communicate on our findings. The work is still very much in process and I shall present hardly any theorems. In particular we still have no strategy that seems promising for obtaining lower bounds. If time allows, I shall briefly mention some results I have obtained on optimal proof systems, a topic not related to the title of this talk.

11:35-12:15 Speaker: Markus Latte; Title: On a method towards a lower bound for intuitionistic logic

Abstract: Normalization is an essential tool for analyzing proofs in natural
deduction style.  We combine this technique with the well known
superpolynomial lower bound for the size of a monotone circuit
deciding the k-clique problem.  For this purpose we construct
a sequence of formulas.  Any normal derivation of anyone of them
specifies a monotone circuit for the clique problem.  To assign
a circuit to a such derivation we consider the normalization process
in reverse order.  This process allows us to backtrack essential
information visible in the normal form back to an arbitrary
derivation.  Finally we show how a small monotone circuit for the
clique problem can be extracted from derivations satisfying some
technical conditions.

14:00-14:40 Speaker: Alan Skelley; Title: Third-order computation and bounded arithmetic, and strong propositional proof systems

Abstract: Several authors have used higher-order theories of bounded arithmetic as a more elegant way of reasoning about some complexity classes. I will discuss one way to extend this to PSPACE and classes from the EXP-time hierarchy, and a reasonable generalization of ordinary computation that fits in nicely. I will then talk about some strong propositional proof systems designed to translate these theories.

14:40-15:20 Speaker: Marta Bilkova; Title: Feasible interpolation in modal logic

Abstract: We shall present a simple proof of feasible disjunction property for modal
logics K, T, K4, S4, GL, and S4Grz. The main advantage of the argument
which is based on modal sequent calculi is that it does not require full
cut elimination.
As a corollary we obtain feasible interpolation theorem and discuss its
complexity consequences.

15:40-16:20 Speaker: Vitezslav Svejdar; Title: On Systems with Rosser Symbols

Abstract: We review some properties and aspects of modal
propositional logic with symbols for witness comparison.

16:20-17:00 Speaker: Pavel Hrubes; Title: A propositional system with a non-trivial upper bound on the number of proof-lines

Abstract: We show that in a propositional proof system SFI the number of proof lines
of a tautology A depends only on the number of propositional variables in A and
not on the size of A. In particular, there is a constant c s.t. every tautology
with no propositional variables (i.e., containing only the atoms 0 and 1) has a
SFI-proof with c proof-lines.

Thursday 12-1-2006

10:00-10:40 Speaker: Mathias Baaz; Title: Herbrand's Theorem and Skolem Functions

Abstract: In this lecture we discuss the connection between Herbrand's Theorem and the
admissability of Skolem Functions both for nonclassical logics and nonstandard
classes of skolem functions. We derive for classical logic a correspondence
between admitted properties of Skolem functions and bounds for the length of
the herbrand disjunction.

10:40-11:20 Speaker: Arnold Beckmann; Title: Continuous cut-elimination and bounded arithmetic

Abstract: This will be an informal talk reporting about some
work in progress.  Continuous cut-elimination is a method
introduced by Mints into Schuette's infinitary cut-elimination
which allows to extract finitary information from infinitary
proofs.  One main use is to extract informations about provable
total functions of theories by infinitary methods.  In the talk
we will try to explain how continuous cut-elimination can be
adapted to proof systems related to bounded arithmetic theories.
One application of this is to extract definable functions in
bounded arithmetic.

11:35-12:15 Speaker: Rosalie Iemhoff; Title: Skolemization, existence and equality

Abstract: Like in classical logic, Skolemization is sound and complete for
prenex formulas in intuitionistic logic. This no longer holds for
infix formulas. We define an alternative Skolemization method that
makes use of an existence predicate and that is sound and complete
for a large class of formulas. It even is so in the presence of
equality, for which Skolemization in intuitionistic is not even
sound and complete for implications between prenex formulas. This
is joint work with Matthias Baaz.

14:00-14:40 Speaker: Petr Hájek; Title: On Grzegorczyk’s weak essentially undecidable theory

Abstract: Grzegorczyk has suggested to study the theory (call it Q−) which results from Robinson’s arithmetic Q by replacing the operations of addition and multiplication by ternary predicates A and M and rewriting the axioms postulating only that A and M are possibly partial functions. He conjectured that the theory is essentially undecidable. I sketch a proof of the positive answer.

14:40-15:20 Speaker: George Metcalfe; Title: Proof Systems for Admissibility

Abstract: The admissible rules of a logic are the rules under which a logic is
closed. In classical logic all admissible rules are also derivable, but in
intuitionistic and many other non-classical logics this is not the case.
Sets of rules (called bases) that added to a logic characterize the set of
admissible rules of that logic have been found for intuitionistic and
various modal and intermediate logics. In this talk we introduce
Gentzen-style proof systems for admissiblility in these logics; the key
idea being that we consider collections (called r-hypersequents) of both
sequents and negated sequents.

15:40-16:20 Speaker: Evan Goris; Title: Logic of Proofs

Abstract: Artemov's Logic of Proofs (LP) is a propositional modal logic, syntactically in the spirit of PDL in the sense that it has a recursively generated set of modalities. LP has many applications of which I will discuss two. First LP can be seen as an explicit version of the modal logic S4. Second LP has an arithmetical interpretation in the spirit of provability logic but where Skolem functions for the existential quantifiers (over proof codes) are brought into the modal language. Combing the above gives an arithmetical interpretation to the modal logic S4. Additionally LP is known to be arithmetically complete for a wider range of theories (most notably Buss' S12) than GL.

16:20-17:00 Speaker: Jan Krajicek; Title: Proof complexity and cryptography

Abstract: I shall discuss to which extend it might be
possible to base security of cryptosystems on
proof complexity hardness. It is an application of
proof complexity generators.

Previous postings

A Preliminary schedule can be found here.

VISITORS: HOTEL arrangements are being taken care of. In case of questions or changes, contact Pavel Hrubes. (pahrubes "include here at"

VISITORS: COMPUTER FACILITIES will consist of using the machines of one of the "locals". It is also possible to have the Mac or IP address of your laptop registered. Like this, you will have access with limited permissions with your laptop on the local network. If you want to register your laptop, send your Mac and/or IP address to Pavel Pudlák (pudlak "include here at" asap.

SPEAKERS: please send asap title + little abstract to Joost J. Joosten (jjoosten "include here at" We will schedule 40 minutes per talk including discussion. So, either prepare a 30 or a 35 minutes presentation.

ALL: FURTHER INFORMATION about the workshop will be posted on this page.

Joost Joosten
Last modified: Wed Jan 11 00:52:24 MET 2006