<?xml version="1.0" encoding="utf-8"?>
<export-example>
  <doc>
    <id>34543</id>
    <completedYear/>
    <publishedYear>2024</publishedYear>
    <thesisYearAccepted/>
    <language>eng</language>
    <pageFirst>39:1</pageFirst>
    <pageLast>39:20</pageLast>
    <pageNumber/>
    <edition/>
    <issue>311</issue>
    <volume/>
    <type>conferenceobject_ref</type>
    <publisherName>Leibniz-Zentrum für Informatik</publisherName>
    <publisherPlace>Schloss Dagstuhl</publisherPlace>
    <creatingCorporation/>
    <contributingCorporation/>
    <belongsToBibliography>0</belongsToBibliography>
    <completedDate>2024-11-13</completedDate>
    <publishedDate>--</publishedDate>
    <thesisDateAccepted>--</thesisDateAccepted>
    <title language="eng">Coinductive techniques for checking satisfiability of generalized nested conditions</title>
    <abstract language="eng">We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a tableau must be fair, where fairness requires that all parts of a condition are processed eventually. Since the correctness arguments are non-trivial, we rely on coinductive proof methods and up-to techniques that structure the arguments. We distinguish between two types of categories: categories where all sections are isomorphisms, allowing for a simpler tableau calculus that includes finite model generation; in categories where this requirement does not hold, model generation does not work, but we still obtain a sound and complete calculus.</abstract>
    <parentTitle language="eng">35th International Conference on Concurrency Theory (CONCUR 2024),  Leibniz International Proceedings in Informatics (LIPIcs)</parentTitle>
    <identifier type="doi">10.4230/LIPIcs.CONCUR.2024.39</identifier>
    <enrichment key="BTU">an der BTU erstellt / created at BTU</enrichment>
    <enrichment key="Publikationsweg">Open Access</enrichment>
    <enrichment key="opus.source">publish</enrichment>
    <enrichment key="Fprofil">2 Gesundheit und Lifes Sciences / Health and Life Sciences</enrichment>
    <enrichment key="Fprofil">4 Künstliche Intelligenz und Sensorik / Artificial Intelligence and Sensor Technology</enrichment>
    <enrichment key="opus.doi.autoCreate">false</enrichment>
    <enrichment key="opus.urn.autoCreate">false</enrichment>
    <author>
      <firstName>Lara</firstName>
      <lastName>Stoltenow</lastName>
    </author>
    <submitter>
      <firstName>Sandy</firstName>
      <lastName>Schneider</lastName>
    </submitter>
    <author>
      <firstName>Barbara</firstName>
      <lastName>König</lastName>
    </author>
    <author>
      <firstName>Sven</firstName>
      <lastName>Schneider</lastName>
    </author>
    <author>
      <firstName>Andrea</firstName>
      <lastName>Corradini</lastName>
    </author>
    <author>
      <firstName>Leen</firstName>
      <lastName>Lambers</lastName>
    </author>
    <author>
      <firstName>Fernando</firstName>
      <lastName>Orejas</lastName>
    </author>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>satisfiability</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>graph conditions</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>coinductive techniques</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>category theory</value>
    </subject>
    <collection role="institutes" number="1206">FG Praktische Informatik / Softwaresystemtechnik</collection>
  </doc>
</export-example>
