Authors: David Cerna and Michael Lettmann
Paper Information
Title: | Towards the Automatic Construction of Schematic Proofs |
Authors: | David Cerna and Michael Lettmann |
Proceedings: | PARIS Contributed papers |
Editors: | Alexis Saurin, David Baelde and Radu Calinescu |
Keywords: | inductive theorem prover, proof schema, Hyper sequents, Leveled sequents |
Abstract: | ABSTRACT. In recent years \emph{schematic representations} of proofs by induction have been studied for there interesting proof theoretic properties, i.e.\ allowing extensions of Herbrand's theorem to certain types of inductive proofs. Most of the work concerning these proof theoretic properties presented schematic proofs as sets of proofs connected by \emph{links} together with a global soundness condition. Recently, the $\mathcal{S}\mathit{i}\mathbf{LK}$-calculus was introduced which provides inferences for expanding the sets of proofs within a schematic proof as well as introducing links without violating the soundness condition. In this work we discuss a simplification of the $\mathcal{S}\mathit{i}\mathbf{LK}$-calculus which isolates the essential mechanisms and provides a path towards the automated construction of schematic proofs. |
Pages: | 6 |
Talk: | Jul 07 14:45 (Session 28J: Contributed talks) |
Paper: |