TY - GEN A1 - Stoltenow, Lara A1 - König, Barbara A1 - Schneider, Sven A1 - Corradini, Andrea A1 - Lambers, Leen A1 - Orejas, Fernando T1 - Coinductive techniques for checking satisfiability of generalized nested conditions T2 - 35th International Conference on Concurrency Theory (CONCUR 2024), Leibniz International Proceedings in Informatics (LIPIcs) N2 - 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. KW - satisfiability KW - graph conditions KW - coinductive techniques KW - category theory Y1 - 2024 U6 - https://doi.org/10.4230/LIPIcs.CONCUR.2024.39 IS - 311 SP - 39:1 EP - 39:20 PB - Leibniz-Zentrum für Informatik CY - Schloss Dagstuhl ER -