  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
