slideshow 3

Logic seminar

usually takes place each Monday at 16:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

Lengths of proofs for Presburger arithmetic
Fedor Pakhomov
Institute of Mathematics
Monday, 7. October 2019 - 13:30 to 15:00
Speedups (i.e., differences in the lengths of shortest proofs of the same sentences) between various theories in the language of first-order arithmetic and richer languages is a relatively well-studied phenomenon. There are three typical orders of speedup that occur in natural examples: non-recursive speedups, at most polynomial speedups, and speedups of the order of the super-exponentiation function exp*(0)=1, exp*(x+1)=exp(exp*(x)).

In the present talk I will compare this situation to what happens over the language of Presburger arithmetic. We consider theories that are complete in the language of Presburger arithmetic and for them the usual quantifier elimination algorithm guarantees that any formula of the length n has a proof of the length ≤exp(exp(exp(P(n)))). This shows that speedups in this setting are at most triple-exponential. An important tool for proving non-polynomial speedups for first-order theories is Friedman-Pudlak finite version of Gödel's second-... more

Clause Set Cycles and Induction
Jannik Vierling
TU Wien
Monday, 30. September 2019 - 13:30 to 15:00
The subject of automated inductive theorem (AITP) proving focuses on the development of procedures that find proofs by induction and their efficient implementation. AITP is of particular relevance to the formal verification of hardware and software. This subject is characterized by a great variety of approaches that are often only empirically studied and their theoretical properties are therefore often unclear. We aim at studying existing approaches to automated inductive theorem proving by applying results from mathematical logic in order to gain a better understanding of the various methods and to explore the relations between them.

In this talk I will present the notion of clause set cycles — an abstraction of the n-clause calculus introduced by Kersani and Peltier in 2013. I will explain this formalism in terms of theories of induction and discuss how the study of this formalism is related to subtheories of Presburger arithmetic.

An exponential lower bound for lengths of proofs in substructural logics
Raheleh Jalali Keshavarz
Institute of Mathematics
Monday, 23. September 2019 - 13:30 to 15:00
In this talk, we will investigate the lengths of proofs in the usual Gentzen calculus for the substructural logic FL_e. We will present a sequence of tautologies of the system and show any short proof for them implies a short proof for Hrubes' formulas for intuitionistic logic, hence the exponential lower bound follows. We will then conclude that this lower bound also applies to any proof system for a logic between FL_e and IPC.

Bounded-depth Frege complexity of Tseitin formulas for all graphs
Nicola Galesi
University of Rome Sapienza
Monday, 16. September 2019 - 13:30 to 15:00

We prove that Tseitin formulas Ts(G), for an undirected graph G, require proofs of size 2^{tw(G)^{\Omega(1/d)}} in depth d-Frege systems for d<{K \log n}/{\log \log n}, where tw(G) is the treewidth of G and K a constant. If time will allow, we prove tightness of the lower bound. Namely, that for large enough d, there are depth d-Frege proofs for Ts(G) of size 2^{\tw(G)^{\O(1/d)}} \poly(|Ts(G)|).This is a joint work with Dmitry Itsykson, Artur Riazanov and Anastasia Sofronova

Pages