Living Without Beth and Craig: Explicit
      Definitions and Interpolants without Beth
        Definability and Craig Interpolation
                        (Abstract of Invited Talk)

                                    Frank Wolter

               University of Liverpool, UK, wolter@liverpool.ac.uk

In logics with the Craig interpolation property (CIP) the existence of an inter-
polant for an implication follows from the validity of the implication. In logics
with the projective Beth definability property (PBDP), the existence of an ex-
plicit definition of a relation follows from the validity of a formula expressing
its implicit definability. From an algorithmic viewpoint, the CIP and PBDP are
of interest because they reduce existence problems to validity checking: an in-
terpolant exists if, and only if, an implication is valid and an explicit definition
exists if, and only if, a straightforward formula stating implicit definability is
valid. The interpolant and explicit definition existence problems are thus not
harder than validity.
    While many logics enjoy the CIP and the PBDP (for instance, first-order logic
(FO), propositional logic, intuitionistic logic, and many modal and description
logics), there are also many important logics that neither enjoy the CIP nor the
PBDP. Examples include modal and description logics with nominals, the two-
variable fragment of FO, the guarded fragment of FO, and most Horn-fragments
of modal and description logics. In this talk, I will present recent results on
the decidability and complexity of interpolant and explicit definition existence
for logics that do not enjoy the CIP nor PBDP. For example, we show that the
existence of explicit definitions of concept names (and individual names) relative
to an ontology in the extension ALCO of ALC with nominals is 2ExpTime-
complete and that the existence of explicit definitions of relation in the guarded
fragment is 3ExpTime-complete, thus in both cases by one exponential harder
than deduction. The presentation is based on [1,3,2].


References
1. Artale, A., Jung, J.C., Mazzullo, A., Ozaki, A., Wolter, F.: Living without Beth
   and Craig: Explicit definitions and interpolants in description logics with nominals
   and role hierarchies. In: Proc. of AAAI (2021)
2. Fortin, M., Konev, B., Wolter, F.: Interpolants and explicit definitions in horn de-
   scription logics (extended abstract). In: Proc. of DL Workshop (2021)
3. Jung, J.C., Wolter, F.: Living without Beth and Craig: Definitions and interpolants
   in the guarded and two-variable fragments. In: Proc. of LICS (2021)

  Copyright © 2021 for this paper by its authors. Use permitted under Creative
  Commons License Attribution 4.0 International (CC BY 4.0).