Towards the Automatic Construction of Schematic Proofs

Description

In recent years schematic representations of proofs by induction have been studied for their 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 links together with a global soundness condition. Recently, the SiLK-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 SiLK-calculus which isolates the essential mechanisms and provides a path towards the automated construction of schematic proofs.

Period	08 Jul 2018
Event title	PARIS 2018
Event type	Conference
Location	United KingdomShow on map