This talk is about the "characteristic clause sets" of sequent
calculus proofs (for first-order classical logic) and about their
expressiveness as a similarity criterion for proofs.
The characteristic clause sets have first been introduced in order
to study cut-elimination: They are used as the main tool of the
cut-elimination method Ceres (Baaz,Leitsch 2000).
In this talk we will present recent results and work in progress
1) on the class of proofs having the same characteristic clause sets and
2) on proofs having strongly related (in the sense of subsumption) clause sets.
We will show that the characteristic clause sets are invariant under a number
of syntactic transformations of sequent calculus proofs that are generally
perceived not to change the character of the mathematical argument
underlying the proof (e.g. NNF-Transformation, rule permutations,...).
Furthermore we will give a comparison to other techniques used for analyzing
the questions of equality and similarity of proofs.