[Back]

S. Hetzl:
"A Similarity Criterion for Proofs (abstract)";
Talk: Computability in Europe 2006, Logical Approaches to Computational Barriers, Swansea, Wales; 2006-06-30 - 2006-07-05; in: "Logical Approaches to Computational Barriers", A. Beckmann, U. Berger, B. Löwe, J. Tucker (ed.); University of Wales Swansea Report Series, CSR 7-2006 (2006), ISBN: 0-86076-189-4; - 295.

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 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 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.

http://publik.tuwien.ac.at/files/pub-inf_4269.pdf