
Neil Thapen

(Institute of Mathematics)

Semantic cutting planes with small coefficients
 Abstract:

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.

Michael Benedikt

(University of Oxford)

Interpolation for Query Reformulation
 Abstract:

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 treeautomata, with some tentative remarks about how these stack up against the requirements.
Pavel Pudlak, Neil Thapen
organizers