The logical method proposed by Goubault, Ledent, and Rajsbaum provides a novel way to show the unsolvability of distributed tasks by means of a logical obstruction, which is an epistemic logic formula describing the reason of unsolvability. In this paper, we introduce the notion of partial product update, which refines that of product update in the original logical method, to encompass distributed tasks and protocols modeled by impure simplicial complexes. With this extended notion of partial product update, the original logical method is generalized so that it allows the application of logical obstruction to show unsolvability results in a distributed environment where the failure of agents is detectable. We demonstrate the use of the logical method by giving a concrete logical obstruction and showing that the consensus task is unsolvable by the single-round synchronous message-passing protocol.

翻译：Goubault，Ledent和Rajsbaum提出的逻辑方法提供了一种新的方式来通过逻辑阻碍来显示分布式任务的不可解性，逻辑阻碍是一种表述不可解性原因的认识逻辑公式。在本文中，我们引入了部分乘积更新的概念，它优化了原始逻辑方法中的乘积更新的概念，以包括由不纯的单纯复合体建模的分布式任务和协议。通过这个扩展的部分乘积更新概念，我们推广了原始逻辑方法，使其可以将逻辑阻碍应用于可检测到代理的分布式环境中，从而展示了不可解性的结果。我们通过提供具体的逻辑阻碍并展示单轮同步传输协议下的共识任务是不可解的来演示逻辑方法的使用。