A compact representation of proofs (Q1102282)

To save information that could be extracted from automatically generated proofs, structures called expansion trees are introduced. These trees provide a computationally useful representation of proofs in classical first-order logic and some of its extensions. Moreover, they can be easily manipulated and transformed. Explicit transformations are presented between expansion tree proofs and cut-free proofs in the sequential calculus. Similar transformations are possible also into Craig style linear proofs giving interpolants whenever they exist. A fragment of simple type theory is used as underlying logic. A stronger form of first-order interpolation theorem is proved and a correct description of Skolem functions and the Herbrand universe is provided.