<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Living Without Beth and Craig: Explicit Definitions and Interpolants without Beth Definability and Craig Interpolation</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>(Abstract of Invited Talk)</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>University of Liverpool</institution>
          ,
          <country country="UK">UK</country>
        </aff>
      </contrib-group>
      <abstract>
        <p>In logics with the Craig interpolation property (CIP) the existence of an interpolant for an implication follows from the validity of the implication. In logics with the projective Beth definability property (PBDP), the existence of an explicit 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 interpolant 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 twovariable 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 2ExpTimecomplete 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].</p>
      </abstract>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <surname>Artale</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Jung</surname>
            ,
            <given-names>J.C.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Mazzullo</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Ozaki</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Wolter</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          :
          <article-title>Living without Beth and Craig: Explicit definitions and interpolants in description logics with nominals and role hierarchies</article-title>
          .
          <source>In: Proc. of AAAI</source>
          (
          <year>2021</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <surname>Fortin</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Konev</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Wolter</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          :
          <article-title>Interpolants and explicit definitions in horn description logics (extended abstract)</article-title>
          .
          <source>In: Proc. of DL Workshop</source>
          (
          <year>2021</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <surname>Jung</surname>
            ,
            <given-names>J.C.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Wolter</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          :
          <article-title>Living without Beth and Craig: Definitions and interpolants in the guarded and two-variable fragments</article-title>
          .
          <source>In: Proc. of LICS</source>
          (
          <year>2021</year>
          )
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>