Logical Approaches to Computational Barriers

A Similarity Criterion for Proofs

Speaker:
| Stefan Hetzl |

Slot: |
Array, 17:20-17:40, col. 3 |

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.

websites: Arnold Beckmann | 2006-05-01 |