I've thought a lot about your question for about 5 years now. My current approach after tonight's brainstorm session is something like this:
What I did was flip to some small definition or theorem in my Topos Theory book by Johnstone, and there's one that goes:
Corollary. A topos is balanced (i.e. a morphism which is both mono and epi is an isomorphism).
So, I thought about how I would represent this definition in a general way so that the approach applies to many other definitions / theorems.
Here are some notes about the image:
The $C:\text{Cat}$ and the $f: \text{Mor}(C)$ are like logic gates on a mosfet transistor. Current can only flow if the gate is activated.
So the definition in usual text form is something like:
$$
\forall C:\text{Cat}, (C \text{ is balanced} \iff \forall f\in \text{Mor}(C), (f \text{ is mono & epi} \iff f \text{ is an isomorphism}))
$$
Now the grey arrows disappear when the user views this definition visually. For example, the "and" node contains two pointers, one to the "f mono" node and one to the "f epi" node. So when you present this to the user you get something more like:
f mono
f epi <=f:Mor(C)=> f isom
But I expanded to the internal workings of the involved data structures for us, in that image.
Now the green text is probably just that: text strings. You parse out variables from them using a regex definition of variable or use a parser generator to define your variable syntax.
Internally, how this works is, when the user asserts that $C$ is a category, the first gate in the image gets activated, so if in addition they say that $C$ is balanced, then a signal (just a function call) triggers the definition expansion node (the stuff on the right) to activate. So then if in addition, if asserted or derived, somewhere along the line that $f$ is a morphism in $C$, as well as being mono and epi, then the conclusion is that $f$ is an isomorphism.
If you were to collect a bunch of these definitions and theorems into a single C++ driven graph, then activation of the relevant graph nodes would trigger an "electrical storm" through the graph, kind of like how our brains work.
That I think would be a very performant search method for searching for "what results if I assume X, Y, and Z"?
So given this design, what your visual graph needs to represent, and what you wont' find in current graph visualization architectures is Node-to-Node, Arrow-to-Node, and Arrow-to-Arrow connections. However, since you're already wanting to support categorical constructions, you'd need to support these connection types anyway! So you have the Commutative Diagram side of things, but you retrofit your diagram editor so that you can also visualize the logic engine nodes.
What's interesting about this approach, is that there exists only one node (unique) with the content $f \text{ epi}$ for example. You don't have one for each possible variable $f$, you use DeBruijn-like indexing in order to get a canonical form for the expression.
I still haven't figured out how to implement this myself, with all the variable substitution tracking that has to happen. Let's work together on this, or brainstorm even further.
One last thing, you should probably also support nesting of arrows and nodes within other nodes as well as node boxes at the $\implies$ and $\iff$ gates. You could probably do it without nesting as well. But then you definitely would need Arrow-to-Node and Arrow-to-Arrow connections.
