Time: 11:00am - 12:00pm Venue: CS 414 4th Floor, Computer Science Bldg Queen Mary, University of London Mile End London E1 4NS
Making First-Order Model Theory Effective
Many of the basic results in the model theory of first order logic state state that properties of structures satisfying some condition can be expressed in a particular syntactic form. Preservation theorems, for example, state that first-order properties whose models are invariant under particular operations (e.g. extension) can be rewritten into a special syntactic form (e.g. as existential formulas); the Beth Definability Theorem states that properties that are “Implicitly Definable” over a subset of the signature can be rewritten as explicit definitions using only that subset. All of these results are proved using non-constructive techniques, and it is easy to show that none of these transformations can be effective.
We revisit these “rewriting properties” for restricted fragments of first order logic, focusing on two fragments that are known to be decidable: the Guarded Fragment (GF) and the Guarded Negation Fragment (GNF) introduced in 2011 by Barany, ten Cate, and Segoufin. We show that many interesting rewriting-related properties hold constructively for GF and GNF. We give effective versions of preservation theorems, and effective generalizations of Beth Definability along with several related results of interest in theorem-proving, description logics, and databases: Craig Interpolation and rewritability of determined views. We also investigate rewriting properties related to the “certain answers” of queries with respect to GNF and GF dependencies, which have received attention for ontological reasoning and data exchange: we show that the certain answers transformation has a particularly simple form in this setting.
This is joint work with Vince Barany of LogicBlox and Balder ten Cate of UC-Santa Cruz.