Proof Schemata
摘要
So far we have seen that terms, formulas, and even substitutions can be defined schematically. This can also be done for proofs. In this chapter we will introduce proof schemata for \(\textbf{LK}\) derivations and resolution refutations.