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.

Attachment

Video Recording