一句话：为描述非纯单纯复形的三值多主体认知逻辑给出公理化，并证明其可靠性与完全性。
组合拓扑被用于分布式计算中建模并发与异步。纯单纯复形描述所有进程存活时的异步消息传递；非纯单纯复形则描述进程可能已死的同步消息传递。其性质可由三值多主体认知逻辑刻画，第三值表示未定义公式，例如死亡主体的知识与局部命题。本文为这类非纯复形对应的逻辑提出公理化系统，并证明可靠性与完全性。完全性证明构造了新的典范单纯模型，且需要谨慎处理未定义公式。
Combinatorial topology is used in distributed computing to model concurrency and asynchrony. The basic structure in combinatorial topology is the simplicial complex, a collection of subsets called simplices of a set of vertices, closed under containment. Pure simplicial complexes describe message passing in asynchronous systems where all processes (agents) are alive, whereas impure simplicial complexes describe message passing in synchronous systems where processes may be dead (have crashed). Properties of impure simplicial complexes can be described in a three-valued multi-agent epistemic logic where the third value represents formulae that are undefined, e.g., the knowledge and local propositions of dead agents. In this work we present an axiomatization for the logic of the class of impure complexes and show soundness and completeness. The completeness proof involves the novel construction of the canonical simplicial model and requires a careful manipulation of undefined formulae.
@article{paperbot2191,
title = {Impure Simplicial Complexes: Complete Axiomatization},
author = {Rojo Randrianomentsoa and Hans van Ditmarsch and Roman Kuznets},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:3)2023}
}