slideshow 3

Logic seminar

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

Proof mining in bounded arithmetic, part 2

Amir Tabatabai
AVCR and Charles University
Monday, 19. February 2018 - 14:00 to 15:30
A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will explain the basics of the theory of computational flows and how they make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof into a sequence of computational reductions by which we can extract the computational content of the low complexity statements in some bounded theories of arithmetic such as I Delta_0, T^k_n, I Delta_0+EXP and PRA.

Proof mining in bounded arithmetic

Amir Tabatabai
AVCR and Charles University
Monday, 5. February 2018 - 14:00 to 15:30
A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will explain the basics of the theory of computational flows and how they make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof into a sequence of computational reductions by which we can extract the computational content of the low complexity statements in some bounded theories of arithmetic such as I Delta_0, T^k_n, I Delta_0+EXP and PRA.

Semantic cutting planes with small coefficients

Neil Thapen
Institute of Mathematics
Monday, 15. January 2018 - 14:00 to 15:30
Cutting planes (CP) is a proof system whose lines are linear integral inequalities. It was shown recently by Filmus, Hrubes and Lauria that a semantic version of CP (that is, allowing any sound rule) is exponentially stronger than usual CP. I will discuss some upper bounds on the refutational and implicational completeness of CP, and show from these that semantic CP can be simulated by CP, if we only consider semantic refutations with very small coefficients. Joint work with Massimo Lauria.

Interpolation for Query Reformulation

Michael Benedikt
University of Oxford
Monday, 4. December 2017 - 14:00 to 15:30
In this talk I will explain query reformulation problems - given a formula Q and a background theory T, the goal is to translate Q, either into another formula or a direct procedural implementation, such that the translation is equivalent to Q according to T, and such that the translation satisfies additional "interface restrictions" - e.g. restrictions on the vocabulary. I will review the approach to solving these problems via interpolation which has been investigated over the last few years, presenting the properties of a proof system and interpolation algorithm we might desire for the application to reformulation. I will then look at some proof methods and associated interpolation algorithms that have been proposed in the past -- via tableaux, resolution, and tree-automata, with some tentative remarks about how these stack up against the requirements.

Pages