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.

翻译：我们研究嵌套条件，这是将一阶逻辑推广到范畴化背景的广义形式，并提出一种基于表（半判定）过程来检验（不）可满足性及生成有限模型。这推广了早期关于图条件的结果。此外，我们引入见证概念，使得在某些情况下能够检测无限模型。为保证完备性，表中的路径必须满足公平性，即要求条件的所有部分最终都能被处理。由于正确性论证并非平凡，我们依赖于共归纳证明方法及结构化论证的"直至"技术。我们区分两类范畴：所有截面均为同构的范畴，允许包含有限模型生成的简化表演算；在此要求不成立的范畴中，模型生成虽不可行，但我们仍能获得可靠且完备的演算系统。