一句话：提出分层图逻辑 ILGL，建立其 Kripke/关系/代数语义与可靠完备表列系统，证明可判定性、对偶并扩展至谓词版本。
复杂系统常以图结构上的分层建模。本文提出直觉主义子结构逻辑 ILGL 来刻画分层：它在直觉主义连接词之外引入非交换、非结合合取及其蕴含，形成 bunched 系统。作者给出图上 Kripke 语义，并证明带标签表列系统的可靠性与完备性；随后建立等价的关系语义，并通过表示定理与代数语义等价。利用该结果，作者由代数语义的有限嵌入性质证明逻辑可判定，并证明 Stone 型对偶。最后引入 ILGL hyperdoctrine 与索引分层框架，将结果扩展到谓词版本，证明扩展分层图语义的可靠性与完备性，并以资源标签 bigraph 模型说明其应用。
Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic called ILGL that gives an account of layering. The logic is a bunched system, combining the usual intuitionistic connectives, together with a non-commutative, non-associative conjunction (used to capture layering) and its associated implications. We give soundness and completeness theorems for a labelled tableaux system with respect to a Kripke semantics on graphs. We then give an equivalent relational semantics, itself proven equivalent to an algebraic semantics via a representation theorem. We utilise this result in two ways. First, we prove decidability of the logic by showing the finite embeddability property holds for the algebraic semantics. Second, we prove a Stone-type duality theorem for the logic. By introducing the notions of ILGL hyperdoctrine and indexed layered frame we are able to extend this result to a predicate version of the logic and prove soundness and completeness theorems for an extension of the layered graph semantics . We indicate the utility of predicate ILGL with a resource-labelled bigraph model.
@article{paperbot361,
title = {Intuitionistic Layered Graph Logic: Semantics and Proof Theory},
author = {Simon Docherty and David Pym},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:11)2018}
}