2026-08-06T11:10:24Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20811 2024-08-29T05:40:58Z ddc:004 open_access

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions Stoltenow, Lara König, Barbara Schneider, Sven Corradini, Andrea Lambers, Leen Orejas, Fernando satisfiability graph conditions coinductive techniques category theory 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lara Stoltenow and Barbara König and Sven Schneider and Andrea Corradini and Leen Lambers and Fernando Orejas 2024 Is Part Of LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2024.39 urn:nbn:de:0030-drops-208113 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.39 eng https://creativecommons.org/licenses/by/4.0/legalcode