<?xml version="1.0" encoding="UTF-8"?>
<OAI-PMH xmlns="http://www.openarchives.org/OAI/2.0/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/ http://www.openarchives.org/OAI/2.0/OAI-PMH.xsd">
  <responseDate>2026-07-25T19:05:29Z</responseDate>
  <request identifier="7678" metadataPrefix="oai_dc" verb="GetRecord">https://drops.dagstuhl.de/oai</request>
  <GetRecord>
    <record>
      <header>
        <identifier>oai:drops-oai.dagstuhl.de:7678</identifier>
        <datestamp>2024-03-06T10:40:45Z</datestamp>
        <setSpec>ddc:004</setSpec>
        <setSpec>open_access</setSpec>
      </header>
      <metadata>
        <oai_dc:dc xmlns:oai_dc="http://www.openarchives.org/OAI/2.0/oai_dc/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/oai_dc/ http://www.openarchives.org/OAI/2.0/oai_dc.xsd">
          <dc:title>Fast(er) Reasoning in Interval Temporal Logic</dc:title>
          <dc:creator>Bresolin, Davide</dc:creator>
          <dc:creator>Muñoz-Velasco, Emilio</dc:creator>
          <dc:creator>Sciavicco, Guido</dc:creator>
          <dc:subject>Temporal Logic</dc:subject>
          <dc:subject>Horn Fragments</dc:subject>
          <dc:subject>Satisfiability</dc:subject>
          <dc:subject>Complexity</dc:subject>
          <dc:description>Clausal forms of logics are of great relevance in Artificial Intelligence, because they couple a high expressivity with a low complexity of reasoning problems. They have been studied for a wide range of classical, modal and temporal logics to obtain tractable fragments of intractable formalisms. In this paper we show that such restrictions can be exploited to lower the complexity of interval temporal logics as well. In particular, we show that for the Horn fragment of the interval logic AAbar (that is, the logic with the modal operators for Allen’s relations meets and met by) without diamonds the complexity lowers from NEXPTIME-complete to P-complete. We prove also that the tractability of the Horn fragments of interval temporal logics is lost as soon as other interval temporal operators are added to AAbar, in most of the cases.</dc:description>
          <dc:publisher>Schloss Dagstuhl – Leibniz-Zentrum für Informatik</dc:publisher>
          <dc:contributor>Davide Bresolin and Emilio Muñoz-Velasco and Guido Sciavicco</dc:contributor>
          <dc:date>2017</dc:date>
          <dc:relation>Is Part Of LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)</dc:relation>
          <dc:type>InProceedings</dc:type>
          <dc:type>Text</dc:type>
          <dc:type>doc-type:ResearchArticle</dc:type>
          <dc:type>publishedVersion</dc:type>
          <dc:format>application/pdf</dc:format>
          <dc:identifier>doi:10.4230/LIPIcs.CSL.2017.17</dc:identifier>
          <dc:identifier>urn:nbn:de:0030-drops-76782</dc:identifier>
          <dc:identifier>https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.17</dc:identifier>
          <dc:language>eng</dc:language>
          <dc:rights>https://creativecommons.org/licenses/by/3.0/legalcode</dc:rights>
        </oai_dc:dc>
      </metadata>
    </record>
  </GetRecord>
</OAI-PMH>
