Higher-order logics and structures (R-6738)

The bulk of the research on the theory of query languages has been guided by the quest for finding a good balance between expressibility and tractability. The most common trend is to start with a weak logic in terms of expressibility over finite models, and to conservatively extend it with different constructs that increase its expressive power. The difficult part is to do this without incurring in big penalties with regards to tractability of the resulting extended language. In this sense, first-order logic extended with different kinds of fixed points and quantifiers such as counting and transitive closure has been extensively studied. Extensions of first-order logic with higher-order quantifiers have not received the same attention in this setting, since existential second-order logic already captures NP. In this project we propose a different approach. Our starting points are higher-order languages which are highly intractable in the general case, but also highly expressive and thus valuable as a tool for high level specification of queries. Then instead of concentrating on ways of making these languages tractable by means of different syntactic restrictions (which would be a more usual approach), we concentrate on ways in which these highly expressive languages can be used to express tractable queries. In this sense, we have identified three promising lines of work.

Keywords:Higher-order logics

Disciplines:Applied mathematics in specific fields

Project type:Collaboration project