Data Compression for Proof Replay
Data Compression for Proof Replay
复制标题
用于验证重放的数据压缩
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Hasan Amjad
中科院分区：
文献类型：
--
作者：
Hasan Amjad
我们描述了SAT求解器产生的命题分辨率的反驳证明对经典自然扣除证明的反驳证明的压缩翻译。通常可以比简单地模拟原始分辨率证明的更快地检查结果证明。我们将此结果用于交互式定理抛弃，以加快SAT求解器生成的证明的重建。翻译很快，并扩展到大量证明，并具有数百万个推论。
We describe a compressing translation from SAT solver generated propositional resolution refutation proofs to classical natural deduction proofs. The resulting proof can usually be checked quicker than one that simply simulates the original resolution proof. We use this result in interactive theorem provers, to speed up reconstruction of SAT solver generated proofs. The translation is fast and scales up to large proofs with millions of inferences.