Hi, I've quickly written an extension to metamath-knife which generates a GraphML file with all theorem dependencies. You can find the PR here:
https://github.com/david-a-wheeler/metamath-knife/pull/112 It adds an option "export-graphml-deps", so that the tool can be called using: metamath-knife set.mm --time --export-graphml-deps deps.xml which generates a "deps.xml" GraphML file. The file generated using the current version of set.mm is around 60Mb, includes 43922 nodes and 1324402 edges. BR, _ Thierry On 04/06/2023 15:14, Humanities Clinic 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 am using macOS10.13.6. May I know, is there any program already written for Metamath that can do this? Otherwise, what would be the fastest/easiest way to achieve the goals I outlined? -- 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/acaf60be-aad3-4e11-9eb4-ecd92479f304n%40googlegroups.com <https://groups.google.com/d/msgid/metamath/acaf60be-aad3-4e11-9eb4-ecd92479f304n%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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/451f9fd1-6b46-3c50-3572-71a717e8d613%40gmx.net.
