Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

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

Hausdorff Center for Mathematics via YouTube

Overview

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.

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

Reviews

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

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.