10 October 2017, Logic Tea, Mauricio Martel
Conservative extensions are a fundamental notion in logic. In the area of descriptionlogic, deciding whether a logical theory is a conservative extension of another theoryis a fundamental reasoning task with applications in ontology modularity and reuse, and ontology versioning. As expected, conservative extensions are undecidable in first-order logic (FO), but it has been observed in recent years that they are decidablein many modal and description logics and that they can often be characterized elegantlyin terms of model theoretic notions. Thus it is natural to ask: Why are conservative extensions in modal and description logics decidable and how far does the decidabilityextend?
In this talk, we consider the decidability of conservative extensions in more expressivedecidable fragments of FO such as the two-variable fragment (FO2) and the guardedfragment (GF). We show that conservative extensions are undecidable in FO2 and in GF, and that they are decidable in the guarded fragment with two variables (GF2). The latter rests on a suitable model-theoretic characterization that is used as a foundation for a decision procedure based on tree automata.
While the talk aims to be accessible to all members of the ILLC a basic familiaritywith computability and complexity theory will be needed to appreciate the talk.