Proof compression
In proof theory, an area of mathematical logic, proof compression is the problem of algorithmically compressing formal proofs. The developed algorithms can be used to improve the proofs generated by automated theorem proving tools such as sat-solvers, SMT-solvers, first-order theorem provers and proof assistants.
The following algorithms are currently known:
- Compression of sequent calculus proofs:
- Compression of propositional resolution proofs:
Notes
- ^ Bar-Ilan, O.; Fuhrmann, O.; Hoory, S. ; Shacham, O. ; Strichman, O. Linear-time Reductions of Resolution Proofs. Hardware and Software: Verification and Testing, p. 114–128, Springer, 2011.
- ^ Bar-Ilan, O.; Fuhrmann, O.; Hoory, S. ; Shacham, O. ; Strichman, O. Linear-time Reductions of Resolution Proofs. Hardware and Software: Verification and Testing, p. 114–128, Springer, 2011.
- ^ Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd International Conference on Automated Deduction, 2011.
- ^ Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd International Conference on Automated Deduction, 2011.
- ^ https://github.com/Paradoxika/Skeptik/tree/develop/doc/papers/LUniv
- ^ Cotton, Scott. "Two Techniques for Minimizing Resolution Proofs". 13th International Conference on Theory and Applications of Satisfiability Testing, 2010.
- ^ Simone, S.F. ; Brutomesso, R. ; Sharygina, N. "An Efficient and Flexible Approach to Resolution Proof Reduction". 6th Haifa Verification Conference, 2010.
 | This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |