Prague-Vienna workshop on Proof Theory and Proof Complexity, 2006
Schedule Prague Vienna Workshop 2006
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 www.mapy.cz.
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" phil.uu.nl) 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" centrum.cz)
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" math.cas.cz) asap.
SPEAKERS: please send asap title + little abstract to Joost J. Joosten (jjoosten "include here at" phil.uu.nl). 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