First-Order Schemata and Inductive Proof Analysis

Schemata are formal tools for describing inductive reasoning. They opened a new area in the analysis of inductive proofs.The book introduces schemata for first-order terms, first-order formulas and first-order inference systems. Based on general first-order schemata, the cut-elimination-by-resolution (CERES) method—developed around the year 2000—is extended to schematic proofs. This extension requ...