[jcranmer]

The actual representation you want wouldn't be a regular graph, but a graph distinguishing theorems and proofs, where the antecedents of theorems are proofs of those theorems, and the antecedents of proofs are theorems they rely on. This kind of graph seems like it should come up regularly enough to have a special name, but I haven't been able to find one.

One important property to note is that a fair number of theorems exist where you can prove A with B or prove B with A, so the underlying directed graph is definitely very cyclic.

[alanbernstein]

Maybe you've encountered it before, but your comment sort of reminds of the concept of a hypergraph (https://en.wikipedia.org/wiki/Hypergraph).

I'm not sure if this is equivalent or related, but I'm imagining an object which can contain, let's call them hypernodes. For example, in the case where A and B mutually imply each other, (A, B) is a hypernode, which internally contains a graph representing the relationship between A and B, but that relationship can be ignored in the main graph. I imagine this would become untenable with a slightly more complex network, though.

[The_rationalist]

A graph whose nodes have for attributes graphs are not an hypergraph. Hypergraph do not modify the definition of a node, only the definition of an (hyper) edge.

From the best AGI project out there: A hypergraph is much like a graph, except that the edges, now called “hyperedges” can contain more than two vertexes. That is, the hyperedge, rather than being an ordered pair of vertexes, is an ordered list of vertexes. The metagraph takes the hypergraph concept one step further: the hyperedge may also contain other hyperedges. https://github.com/opencog/atomspace/blob/master/opencog/she...

[alanbernstein]

Thanks for the clarification, that makes sense. I just would not have been surprised to learn that two different looking extensions of the basic graph concept might turn out to be equivalent, or dual.

[drdeca]

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

[jcranmer]

> 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.