Proof compression

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 and first-order theorem provers and interactive theorem provers.

The following algorithms are currently known:

• Compression of sequent calculus proofs:
  • Cut-Introduction by Resolution
  • Cut-Introduction via Herbrand Sequent Analysis
  • Cut-Elimination
• Compression of propositional resolution proofs:
  • RecyclePivots
  • LowerUnits
  • Resolution Proof Compression by Splitting
  • Resolution Proof Reduction via Local Context Rewriting