> On Jun 4, 2023, at 9:14 AM, Humanities Clinic <[email protected]> > wrote: > > I am stating more specifically the goals I have in mind when I asked: > https://groups.google.com/d/msgid/metamath/CAFXXJSvQt6D6xoufTE5%2BbvyKmfUVN0R0AZK0Ch_7qfLbR95Duw%40mail.gmail.com?utm_medium=email&utm_source=footer > > I need to explore the "graph" of statements in set.mm. Specifically, I need > to (1) find all sinks and sources quickly (2) Isolate one walk/path/trail > between two specified nodes (3a) MOST IMPORTANTLY: With arrow keys on the > keyboard, navigate between adjacent nodes. Up arrow - for the parent of the > node. Down arrow - for the child of the node. Left and right arrows - for the > siblings of the node (3b) I need to explore the subgraph of (only) all > definitions in the way outlined in (3a), so I need to be able isolate this > subgraph from the entire graph.
I think building on Thierry's code will get you there. It's a different visualization, but you might also be interested in my video "Metamath Proof Explorer (set.mm) contributions visualized with Gource through 2020-04-29" at <https://www.youtube.com/watch?v=LVGSeDjWzUo>. This video shows the set.mm database's structure and growth over time. Each little circle represents an assertion (mostly theorems). It's structured by section and subsection, not by internal theorem dependencies. Even so, it may be of interest to you. The code to generate this is all publicly available. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ECFCA016-49FC-4BFE-94D4-F4B27CB75BB9%40dwheeler.com.
