Proof compressions with circuit-structured substitutions

It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between cutfree (or normal) proofs and the corresponding (non-normal) proofs with cuts (or modus ponens). The task of automatic theorem proving is, on the other hand, usually based on the construction of cutfree or only atomic-cuts proofs, since this procedure produces less alternative choices. There are familiar tautologies whose cutfree proofs are huge while the non-cutfree being small. The aim of this paper is to discuss basic methods of weight and/or size reduction of deductions by switching from traditional tree-structured deductions to circuit-structured deductions. A desired efficiency is achieved by adding standard weakening rule of inference upgraded by adding suitable (propositional) unifications modulo variable substitutions. We show examples where such unification provides strong (in fact exponential) compression of cutfree deductions. Bibl. – 10 titles.