Parameterizing the Notion of Automatability in Proof Complexity
Hannah Van Santvliet

Abstract:
In the thesis, we extend the proof-theoretic notion of automatability to a parameterized version called fpt-automatability. Automatability gives an indication whether for a proof system automated theorem search is feasible. We develop parameterized automatability results that enrich the theory of automatability with a collection of graph parameters for the proof systems Extended Frege and resolution. We use methods such as interpolation and polynomial simulation for bounded arithmetic formulas, and we exploit properties for intersection graphs. Also, with fpt-dominance, we show relationships between the parameters.