Title: Proof Simplification for Model Generation and Its Applications
Authors: Miyuki Koshimura, Ryuzo Hasegawa 

Abstract:

Proof simplification eliminates unnecessary parts from a proof
leaving only essential parts in a simplified proof.  This
paper gives a proof simplification procedure for model generation
theorem proving and its applications to proof condensation, folding-up
and completeness proofs for non-Horn magic sets. These indicate
that proof simplification plays a useful role in theorem proving.