Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
WolframInstitute`TuringMachine`InductiveProofs`
multiwaySubProofCones  |
|
| | ||||
▪
A cone is grown for the base case, the step case, and each grafted derived-lemma case; growth is confined to the term-size regime of the proof it envelops so the non-terminating rewrite system does not run away.
▪
The result is an association with keys , , and (the per-case clouds).
"ProofGraph"
"CaseList"
"Cones"
▪
Options include , , , , , , , , and ( or the proof's axioms).
"MaxStates"
"SuperposeGenerations"
"Beam"
"MaxNew"
"SizeBound"
"SizeMargin"
"ThickenAroundProof"
"GraftDerived"
"Axioms"
"Raw"
▪
This is the data measures and embeds the proof into.
multiwayCloudOverlap
MultiwayInductiveProofPanel
Examples
(1)
Basic Examples
(1)
Build the cones for the binary-incrementer machine 453 and list the parts:
In[1]:=
Keys
[453]
 | multiwaySubProofCones |
Out[1]=
{ProofGraph,CaseList,Cones}
 |
|
""