4th JAIST Advanced Lecture Series
Craig Interpolation and Theory Decomposition
Prof. Frank Wolter

Univ. of Liverpool, Guest Prof. of JAIST
http://www.csc.liv.ac.uk/~frank/

リバプール大学 教授
北陸先端科学技術大学院大学 客員教授

Part 1: “Craig Interpolation and Theory Decomposition”
 15:30 - 17:00, September 21 (Tue.) 2010
Part 2:“Towards Dichotomy Results for the Complexity of Subboolean Modal Logics and Lightweight Description Logics”
 15:30 - 16:30, Semtember 22 (Wed.) 2010

KS Lecture Hall , 2nd floor of Knowledge Science 1

Part 1 
Craig‘s interpolation theorem has proved to be a fundamental logical property with numerous applications. In its simplest form, it states that whenever a sentence A implies a sentence B there exists a sentence C, the interpolant, using the shared symbols of A and B only such that A implies C and C implies B. In the first part of this presentation, we give a (very incomplete) survey of results, open problems and applications of the Craig Interpolation property in Logic and Computer Science. The discussion will range from investigating the size of interpolants to applications in model checking and interpolation in non-classical logics.
In the second part, we present recent applications of (variants) of Craig Interpolation to theory decomposition. We will investigate the notion of parallel interpolation introduced by Parikh, Makinson, and Ponomaryov and present its application to computing the unique finest decomposition of theories.

Part 2 
If P does not equal NP, then there are problems whose complexity is properly between P and NP. However, for some important classes of computational problems it is known that no problem in the class is between P and NP. Results of this type are known as dichotomy results and often come with a transparent and complete characterization of the tractable problems within the class. In recent years, many significant dichotomy results have been obtained in the area of constraint satisfaction problems.
In this presentation we focus on recent dichotomy results in modal and description logic. We discuss different ways of formulating the problem and present a number of encouraging results. 

担当者

H.Ono