Data Compression for Proof Replay |
| |
Authors: | Hasan Amjad |
| |
Affiliation: | 1. University of Cambridge Computer Laboratory, William Gates Building, 15 JJ Thomson Avenue, Cambridge, CB3 0FD, UK
|
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|