Proof complexity of systems of (non-deterministic) decision trees and branching programs

TL;DR

This paper explores the proof complexity of propositional systems based on decision trees and branching programs, analyzing their simulation capabilities and comparing them with classical proof systems like Frege systems.

Contribution

It introduces and studies propositional proof systems using deterministic and nondeterministic decision trees and branching programs, providing new simulation and non-simulation results.

Findings

Tree-like and dag-like proof simulations are characterized.

Deterministic and nondeterministic systems differ in proof strength.

Comparison with Frege systems highlights relative efficiencies.

Abstract

This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs - deterministic and nondeterministic. The systems LDT and LNDT are propositional proof systems in which lines represent deterministic or non-deterministic decision trees. Branching programs are modeled as decision dags. Adding extension to LDT and LNDT gives systems eLDT and eLNDT in which lines represent deterministic and non-deterministic branching programs, respectively. Deterministic and non-deterministic branching programs correspond to log-space (L) and nondeterministic log-space (NL). Thus the systems eLDT and eLNDT are propositional proof systems that reason with (nonuniform) L and NL properties. The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in the systems LDT, LNDT, eLDT, and eLNDT. These systems are also compared with Frege systems, constantdepth Frege systems and extended Frege systems