Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
WolframInstitute`TuringMachine`InductiveProofs`
MultiwayTokenEventGraph  |
|
| | ||||
▪
Each rewrite becomes an event vertex fed by the state it rewrites and the axiom it applies, making explicit which axiom drives each step.
▪
The following options can be given:
option | default | description | |
"WellFormedOnly" | True | keep only well-formed configurations | |
"Labeled" | False | draw labelled equation/axiom vertices instead of discs | |
"CollapseAxioms" | False | merge equal axiom applications into one vertex | |
"ShowAxioms" | True | draw the axiom vertices feeding events | |
"HighlightStyle" | "Red" | how the proof path is highlighted ( "Red" "Fade" "Wash" | |
"MaxStates" | Infinity | cap on the number of states explored | |
"Oriented" | False | rewrite downhill only | |
"CriticalPairs" | False | include superposition rules | |
"ArrowSize" | 0.011 | arrowhead size |
Examples
(1)
Basic Examples
(1)
Token-event cloud connecting a ones run to its -appended form:
s1
In[1]:=
 | MultiwayTokenEventGraph |
Out[1]=
 |
|
""