MALL证明等价性是对数空间完备的，通过二元决策图
MALL proof equivalence is Logspace-complete, via binary decision diagrams
摘要：
逻辑中的证明等价问题是判定两个证明是否模一组规则置换等价的问题，这些规则置换反映了其割消过程的交换转换。因此，它与证明网的问题有关：找到具有良好计算特性的等价证明类的规范代表。它也可以看作是自由范畴概念对应于逻辑的语词问题。最近已经表明，MLL（线性逻辑的单位片段的乘法）中的证明等价是PSPACE-完全的，这排除了这种特定逻辑的证明网的任何低复杂度概念。由于它是另一个片段的线性逻辑，试图定义一个完全令人满意的低复杂度的概念证明网还没有成功，到目前为止，我们研究证明等价MALL-（乘法加法没有单位片段的线性逻辑），并发现一种情况是完全不同的MLL的情况。事实上，我们证明在MALL等价对应（根据AC 0减少）等价的二元决策图，一个数据结构广泛用于表示和分析布尔函数有效。我们证明了这两个等价问题是LOGSPACE完备的。如果这在技术上为MALL-的证明网问题的完整解决方案留下了可能性，那么与二元决策图建立的关系实际上表明了这个问题的否定解决方案。
英文摘要：
Proof equivalence in a logic is the problem of deciding whether two proofs are equivalent modulo a set of permutation of rules that reflects the commutative conversions of its cut-elimination procedure. As such, it is related to the question of proofnets: finding canonical representatives of equivalence classes of proofs that have good computational properties. It can also be seen as the word problem for the notion of free category corresponding to the logic. It has been recently shown that proof equivalence in MLL (the multiplicative with units fragment of linear logic) is PSPACE-complete, which rules out any low-complexity notion of proofnet for this particular logic. Since it is another fragment of linear logic for which attempts to define a fully satisfactory low-complexity notion of proofnet have not been successful so far, we study proof equivalence in MALL- (multiplicative-additive without units fragment of linear logic) and discover a situation that is totally different from the MLL case. Indeed, we show that proof equivalence in MALL- corresponds (under AC0 reductions) to equivalence of binary decision diagrams, a data structure widely used to represent and analyze Boolean functions efficiently. We show these two equivalent problems to be LOGSPACE-complete. If this technically leaves open the possibility for a complete solution to the question of proofnets for MALL-, the established relation with binary decision diagrams actually suggests a negative solution to this problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
