##
Making First-Order Model Theory Effective

### Michael Benedikt

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.