Jump to content

Proof compression

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Ceilican (talk | contribs) at 13:10, 15 March 2012 (Added reference for LowerUnits). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

This article does not cite any sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.
Find sources: "Proof compression" – news · newspapers · books · scholar · JSTOR (March 2012) (Learn how and when to remove this message)

Within proof theory, 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:
- Cut-Introduction
- Cut-Elimination
Compression of propositional resolution proofs:

Notes

^ Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd International Conference on Automated Deduction, 2011.

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Proof_compression&oldid=482021321"

Hidden categories: