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.