David Cerna: Proof Schema and the Refutational Complexity of Their Cut Structure
Hausdorff Center for Mathematics via YouTube
Overview
Syllabus
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
Taught by
Hausdorff Center for Mathematics