Tags:automatizability of proof systems, optimal proof systems, proof complexity and propositional proof systems

Abstract:

The problem of the existence of an p-optimal propositional proof system is one of the central open problems in proof complexity.

The goal of this work is to study the restricted case of this problem, namely, the case of strong reductions. We also introduce the notion of bounded proof system and study the connection between optimality and automatizability for bounded proof systems.