[Date Prev][Date Next][Date Index]

*From*: Stefan Woltran <woltran@dbai.tuwien.ac.at>*Date*: Tue, 10 May 2016 13:12:56 +0200

Dear Colleagues, The DBAI Group cordially invites you to the following talk ------------------------------------------------------------------------- Title: On Fragments of Third Order Logic that on Finite Structures Collapse to Second Order Logic Speaker: Flavio Ferrarotti (Software Competence Center Hagenberg (SCCH)) ------------------------------------------------------------------------- Room: Seminarroom 186 (Room-number HA0503) Favoritenstr. 9-11; 5th floor, stairway 1. TU Wien Time: Wed, May 11th, 11:00 c.t. ------------------------------------------------------------------------- Abstract: In the framework of computable queries in Finite Model Theory, there are many examples of properties (queries) that can be expressed by simple and elegant third order logic (TO) formulae. In many of those properties the expressive power of TO is not required, but the equivalent second order logic (SO) formulae can be very complicated or unintuitive. In this talk, we present initial results in the research direction of finding ways to isolate the fragments of TO (and, in general, of higher order logics of order i > 2) formulae which do have an SO equivalent formula. Firstly, we define a general schema of existential TO formulae which consists of existentially quantifying a third order linear digraph of polynomial length, that is, a sequence of structures that represents a computation, by explicitly stating which operations are the ones which can be involved in the construction of a given structure in the sequence, when applied to the previous one. Then we give a constructive proof of the fact that all existential TO sub formulae of that schema can be translated into an equivalent SO formula. We give several examples which show that this is a very usual, intuitive, and convenient schema in the expression of properties. Secondly, aiming to formally characterize the fragment of TO which can be translated to SO, we define a restriction of TO, which we denote TO^P, for polynomial TO, and we give a constructive proof on the fact that it collapses to SO. We define TO^P as the fragment of TO where valuations can assign to TO relation variables only TO relations whose cardinalities are bounded by a polynomial that depends on the quantifier. Short Bio: Dr. Flavio Ferrarotti holds a key-researcher position in the Software Competence Center Hagenberg (SCCH), Austria. He is currently working in the fundamental research projects BLogDAS and HOLS funded by FWF. BLogDAS aims to develop a behavioural theory and logics for distributed adaptive systems. HOLS is a bilateral cooperation project between Austria and Flanders (Belgium) aiming to provide new theoretical insights into the expressive power of higher-order logics as a foundation for modern data models and data manipulation languages. He leads the Austrian side of this project. He holds a Ph.D. in Information Systems from Massey University, New Zealand. He has worked in database theory, finite model theory and rigorous methods. Before joining SCCH, he worked as postdoctoral researcher at Yahoo! research Latin America (two years) and at Victoria University of Wellington in New Zealand (four years).