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

Talk Announcement: Wed May 11, On Fragments of Third Order Logic that on Finite Structures Collapse to Second Order Logic




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).