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 "false." 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??