从类似DAG的证明到精益中的布尔电路
From Dag-Like Proofs to Boolean Circuits in Lean
浏览论文内容
中文总结 AI 辅助
本文提出将通过水平压缩纯蕴含极小逻辑自然演绎证明得到的DLDS编码为布尔电路的方法，定义构建过程并证明正确性，精益形式化提供保证，为自动定理证明和形式认证带来新视角。
中文摘要 AI 辅助
在本文中，我们提出一种方法，将通过对纯蕴含极小逻辑中的自然演绎证明进行水平压缩而获得的类似有向无环图（DAG）的可推导性结构（DLDS）编码为布尔电路。这些DLDS将自然演绎树状证明压缩为有向无环图，在减少冗余的同时保持逻辑正确性。我们正式定义了电路构建过程并证明其逐点正确性。一个精益形式化建立了电路评估器的机器检查保证，并为未压缩的简单树片段提供了一个受限桥梁。这种方法为自动定理证明和形式认证开辟了新视角。
英文摘要
In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), obtained via horizontal compression of Natural Deduction proofs in purely implicational minimal logic, as Boolean circuits. These DLDS compress Natural Deduction tree-like proofs into directed acyclic graphs, preserving logical correctness while reducing redundancy. We formally define the circuit construction process and establish its pointwise correctness, showing that, for any fixed path assignment, the resulting Boolean circuit agrees with the intended dependency-propagation semantics. A Lean formalization establishes machine-checked guarantees for the circuit evaluator and includes a restricted bridge for the uncompressed simple-tree fragment, connecting valid DLDS instances in that fragment to genuine circuit acceptance of their extracted paths under the route and discharge conditions formalized in Lean. This approach opens new perspectives for automated theorem proving and formal certification.
