Read-Once Branching Programs as Proof Lines
4Dmitry Itsykson (Ben-Gurion University of the Negev)
https://simons.berkeley.edu/talks/dmitry-itsykson-ben-gurion-university-negev-2023-03-23-0
Proof Complexity and Meta-Mathematics
We consider refutational semantic proof systems that are defined by the class of predicates that can be used as proof lines; we study lower bounds on size of proofs ignoring the question of verification of the correctness of rules. If we use too strong a model, for example, Boolean formulas, then every unsatisfiable CNF has a short refutation. If we consider too weak a model, for example, decision trees, then the resulting proof system is equivalent to Resolution. In the talk, we discuss cases, where proof lines are represented by read-once branching programs (deterministic, nondeterministic, and ordered, so-called OBDDs). We overview known lower bounds, relations between different types of these proof systems and classical proof systems, and questions of automatability. We also formulate multiple interesting open questions.