Graph that represents logical reasoning

Question

The proof of a statement $X$ in terms of assumptions $A$, $B$ and $C$ can sometimes be represented using a directed graph: $$ \begin{matrix} & & X\\ & \nearrow & & \nwarrow\\ A & & & & Y\\ & & & \nearrow & & \nwarrow\\ & & B & & & & C \end{matrix} $$ where $Y$ is an intermediate conclusion. $p \to q$ means that "$p$ is used in the proof of $q$", not that "$p$ implies $q$".

What is the name of this kind of "reasoning diagram"?

This paper defines something similar called a logical graph; indeed, its Introduction describes exactly what I described above. However the paper later says that arrows mean implication, and the well-formedness conditions in Definition 1 no longer cater to what I described above.

Answer 1

Any formal proof in Hilbert systems, natural deduction systems or sequent calculi can be represented as a "reasoning diagram" of the kind you mentioned. Some authors call these diagrams simply proof trees or deduction trees. As you correctly remarked, the edges between the nodes of a proof tree do in general not correspond to implication.

(Concerning the paper you mentioned, the author seems not to be concerned with proof trees in the usual sense. My first impression is that he only tries to represent single formulas as what he calls a "logical graph" and on page 2, he explicitly says that "edges in the [logical] graph correspond to implication in the formula". Hence, the "logical graphs" in the paper are not the same as proof trees in the usual sense.)

$\textbf{edit:}$ Here is an exemplary explanation of how proof trees for a given proof system (e.g. for propositional logic) can be constructed. Assume we have a proof system $P$ given by some axioms and by a rule, for example Modus Ponens: from $A$ and $A \supset B$, deduce $B$

A proof tree in $P$ can be constructed according to the following two rules:

i) each instance of an axiom of $P$ is a proof tree

ii) if $T_1$ and $T_2$ are proof trees where $T_1$ has a formula $A$ as root and $T_2$ has a formula $A \supset B$ as root, then
$$ \begin{matrix} & & B & \\ & \nearrow & & \nwarrow \\ T_1 & & & & T_2\\ \end{matrix} $$ is a proof tree.

If for a formula $A$, there exists a proof tree with root $A$, then $A$ is called provable in $P$, notation: $\vdash A$.

Note that the proof trees which emerge through this construction are in fact labelled trees (this means in our context that it is possible that two different nodes of a tree are labelled with one and the same formula). Moreover, observe that rule ii) corresponds to the application of modus ponens. A last comment: I included arrows in rule ii) to be consistent with your notation and because I do not know how to draw trees in latex. In fact, you can consider the arrows in rule ii) simply as being edges from the root of $T_1$ resp. $T_2$ to $B$ (i.e. the direction of the edges does not play a role).

Answer 2

You can think of proofs as programs, so you can just call it a dependency graph or call graph.