David Cerna: Proof Schema and the Refutational Complexity of Their Cut Structure

Explore the intricacies of proof schema and their cut structure's refutational complexity in this 39-minute lecture from the Hausdorff Trimester Program on Types, Sets and Constructions. Delve into motivating examples and the mechanisms behind schematic proofs before examining proof schema through comparison. Investigate the Characteristic Clause Set representation in CERES and recursive refutation techniques. Learn about the Cut Structure Inductive Definition (ECA) and its application in Viper. Discover the Inductive Definition of Cut Structure (ANIA) and alternative approaches. Analyze the concept of 1-Strict Monotone Assertion (1-SMA), its hardness, and associated complexity measures. Conclude with insights into future research directions in this field.

Intro
Motivating example
Mechanism behind Schematic Proofs
Proof Schema: by comparison
CERES: The Characteristic Clause Set representation
A Recursive Refutation
ECA: Cut Structure Inductive Definition
Viper And The ECA
NIA: Inductive Definition of Cut Structure
Other than Viper...
A Way Out, 1-Strict Monotone Assertion (1-SMA)
1-SMA: Hardness
Complexity Measure
Conclusions & future work