Sam Buss
    Substitution and Propositional Proof Complexity
    In Alasdair Urquhart on Nonclassical and Algebraic Logic and Complexity of Proofs
    Springer, 2022, pp. 477-496.

    Download preprint.

Abstract: We discuss substitution rules that allow the substitution of formulas for formula variables. A substitution rule was first introduced by Frege. More recently, substitution is studied in the setting of propositional logic. We state theorems of Urquhart's giving lower bounds on the number of steps in the substitution Frege system for propositional logic. We give the first superlinear lower bounds on the number of symbols in substitution Frege and multi-substitution Frege proofs.

Back to Sam Buss's publications page.