Proof Schemata: A Formalism for Proof Transformation in the Presence of Induction
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
The Proof Society Workshop 2018
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Proof schemata are a relatively recent sequent formalism which represents inductive arguments as infinite sequences of finite proofs. While this is similar to Omega rule type sequent formal- isms, proof schemata require an explicit primitive recursive construction of the proof sequence. In contrast to cyclic proof formalisms, proof schemata do not prove statements by infinite de- scent, rather given an tuple of elements from the indexing sort, a proof schema can be normalized to a first order sequent proof. Essentially, proof schemata fall in between these two well known formalisms. However, while these alternative formal- isms both admit cut-elimination and the subformula property, as do proof schemata, they do not extend essential consequences such as Herbrands theorem. Neither system was designed to track particular instances of formula occur- rences. On the other hand, proof schemata excel at occurrence tracking on the benefit of their primitive recursive construction. Though this type of proof construction incur certain difficulties which are not shared with the other formalisms for induction. In this talk we discuss, the state of the art, current investigations, and open problems.
Forschungs-