Graph theoretic restriction to Proofs in Proof Complexity Theory Proof complexity is a most basic area of computational complexity theory. An ultimate purpose of this area is to prove $NP\neq coNP$, that is, any prover cannot give a proof of unsatisfiability of given input formula.
A graph is one of formal model of proofs.  My question is about further restriction to this model.
A proof is represented as a DAG. Nodes with fan-in 0 have axiom-labels. The unique node with fan-out 0 corresponds to &quot;false.&quot; For given input rules of deduction, each node which has both in-degree and out-degree has the  label representing proposition.
My question is:

Are there proof systems and related researches in the case that the class of proof-DAGs are restricted?
Papers, survey, and lecture note are welcome.
Do Proof Systems which are previously studied such as Nullstellensatz, Resolution, LS, AC0 Frege, RES(k), Polynomial Caluculus, and Cutting Planes, have some graph theoretic characterization??
The most natural restriction on the proof DAG is that it be a tree – that is, any "lemma" (intermediate conclusion) is not used more than once. This property is called being "tree-like". General resolution is exponentially more powerful than tree-like resolution, as shown for example by Ben-Sasson, Impagliazzo and Wigderson. The concept has also been considered for other proof systems – just search for "tree-like X", where X is a proof system interesting you. In the particular case of resolution, there are other restrictions that can be considered. See for example a paper of Alekhnovich, Johannsen, Pitassi and Urquhart regarding regular resolution.

Tree-like resolution is especially important since traditional implementations of DPLL correspond to tree-like resolution refutations. The technique of clause learning, which is important in practice, corresponds to allowing general DAGs. Hence the structure of the proof DAG is also strongly dependent on the algorithm generating it.