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

Created from the Publication Database of the Vienna University of Technology.