Schematic Refutations of Formula Schemata

David Cerna, Alexander Leitsch, Anela Lolic

Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define…