Abstract
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.