FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Towards the Automatic Construction of Schematic Proofs

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: