Towards the Automatic Construction of Schematic Proofs
Sprache des Vortragstitels:
Sprache des Tagungstitel:
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.