Is the name you are looking for "bipartite directed graph" ?
Well, specifically, a bipartite directed graph equipped with the specific partition, but if the graph is connected[1], which it should be in this case, then the partition is uniquely defined.
I guess such a graph would define another directed graph which has as vertices, the subsets of the "theorem" vertices, and a directed edge from any such subset to another which has 1 more "theorem" vertex, exactly when the "theorem" vertex has (in the original graph) an antecedent proof vertex such that all of the antecedent theorem vertices of that proof vertex are elements of the original subset of the theorem vertices.
so, if G = (V, E) is the original graph of theorems and proofs, and T \subset V is the set of theorems,
V' := \{ S \subset A \}
\forall S \in V', t \in T, (S, S \cup t) \in E' iff :
t \not\in S, and \exists p \in V s.t. (p,t) \in E, and \forall t' \in T s.t. (t',p) , it holds that t' \in S.
G' := (V', E')
G' _will_ be a directed acyclic graph, because all of the edges strictly increase the size of the set.
Then, finding "how can one learn all the prerequisite proofs in order to learn [result]"
can be rephrased as "given the current vertex of G' (which is the set of theorems one already knows), what is a path which will get to any of the vertices of G' which have as an element the desired element [result] of G ?".
The graph G' would be exponentially large in the size of T, so probably should not be represented explicitly in memory,
but it seems like some shortest path algorithms should still help with this?
There are many other properties of the graph G' which I imagine would be helpful in constructing a shortest path.
[1] in the sense that if you forgot the direction of the edges, the result is connected, not in the sense that every pair of vertices can be connected by a directed path in both directions
> Is the name you are looking for "bipartite directed graph" ?
I've described it as bipartite directed graph in the past, but a key element of what I describe is that the two sets of nodes generally inherit their properties in different ways. For one set, you need something to happen "for all" predecessors; for the other, it needs to happen "for any" predecessor. It's this extra property I have no name for.
Well, specifically, a bipartite directed graph equipped with the specific partition, but if the graph is connected[1], which it should be in this case, then the partition is uniquely defined.
I guess such a graph would define another directed graph which has as vertices, the subsets of the "theorem" vertices, and a directed edge from any such subset to another which has 1 more "theorem" vertex, exactly when the "theorem" vertex has (in the original graph) an antecedent proof vertex such that all of the antecedent theorem vertices of that proof vertex are elements of the original subset of the theorem vertices.
so, if G = (V, E) is the original graph of theorems and proofs, and T \subset V is the set of theorems,
V' := \{ S \subset A \}
\forall S \in V', t \in T, (S, S \cup t) \in E' iff :
G' := (V', E')G' _will_ be a directed acyclic graph, because all of the edges strictly increase the size of the set. Then, finding "how can one learn all the prerequisite proofs in order to learn [result]" can be rephrased as "given the current vertex of G' (which is the set of theorems one already knows), what is a path which will get to any of the vertices of G' which have as an element the desired element [result] of G ?". The graph G' would be exponentially large in the size of T, so probably should not be represented explicitly in memory, but it seems like some shortest path algorithms should still help with this? There are many other properties of the graph G' which I imagine would be helpful in constructing a shortest path.
[1] in the sense that if you forgot the direction of the edges, the result is connected, not in the sense that every pair of vertices can be connected by a directed path in both directions