Combining Proofs to form Different Proofs
Abstract
Different Automated Theorem Proving (ATP) systems solve different parts
of different problems in different ways.
Given a set of proofs produced by ATP systems based on
adequately common principles, it is possible to create new proofs by
combining proof components extracted from the proofs in the set.
It is not generally easy to say that one of the original or new proofs
is better or worse than another, but ways to show that two proofs are
different are available.
This talk describes a process of proof combination to form new proofs
that are different from the original set of proofs.