In[]:=
PacletInstall[CloudObject["https://wolfr.am/10Vhe8A43"],ForceVersionInstall->True]
Out[]=
PacletObject
In[]:=
<<Wolfram`Metamathematics`
“Rotate” the proof object graph
“Rotate” the proof object graph
Display “what got transformed” as part of the event
Display “what got transformed” as part of the event
In TEG for metamathematics ... the tokens are complete math statements
In TEG for metamathematics ... the tokens are complete math statements
Vs. WPP: tokens are terms...
In[]:=
FindEquationalProof[a∘(b∘(c∘d))e∘d,ForAll[{a,b},a==b∘a]]
Out[]=
ProofObject
In[]:=
ProofObjectToTokenEventGraph[%]
Out[]=
In[]:=
EdgeList[%64]
Out[]=
{(e∘da∘(b∘(c∘d))){Event,Substitution Lemma 1},(ab∘a){Event,Substitution Lemma 1},{Event,Substitution Lemma 1}(e∘da∘(b∘d)),(ab∘a){Event,Substitution Lemma 2},(e∘da∘(b∘d)){Event,Substitution Lemma 2},{Event,Substitution Lemma 2}(da∘(b∘d)),(ab∘a){Event,Substitution Lemma 3},(da∘(b∘d)){Event,Substitution Lemma 3},{Event,Substitution Lemma 3}(da∘d),(ab∘a){Event,Conclusion 1},(da∘d){Event,Conclusion 1},{Event,Conclusion 1}(dd)}
In[]:=
If[First[#]=!=(ab∘a),Reverse[#],#]&/@EdgeList[%64]
Out[]=
{{Event,Substitution Lemma 1}(e∘da∘(b∘(c∘d))),(ab∘a){Event,Substitution Lemma 1},(e∘da∘(b∘d)){Event,Substitution Lemma 1},(ab∘a){Event,Substitution Lemma 2},{Event,Substitution Lemma 2}(e∘da∘(b∘d)),(da∘(b∘d)){Event,Substitution Lemma 2},(ab∘a){Event,Substitution Lemma 3},{Event,Substitution Lemma 3}(da∘(b∘d)),(da∘d){Event,Substitution Lemma 3},(ab∘a){Event,Conclusion 1},{Event,Conclusion 1}(da∘d),(dd){Event,Conclusion 1}}
In[]:=
Graph[%,Options[%64]]
Out[]=
In[]:=
VertexDelete[%70,{{"Event","Conclusion 1"}}]
Out[]=
With[{g=AccumulativeTokenEventGraph[{a_<->b_∘a_},2,"S","TokenLabeling"->True]},Subgraph[g,#]&/@findProof[g,{a_<->b_∘a_},a_∘(b_∘(c_∘d_))<->e_∘d_,1]]
The non-accumulative TEG is just like the path-based derivation system ... except that events can be fed by different axioms (if there are multiple axioms)
The non-accumulative TEG is just like the path-based derivation system ... except that events can be fed by different axioms (if there are multiple axioms)
Cut elimination [ cf inlining proofs inside proofs ]
FEP finds a path to get to a given statement from the “big bang”
FEP finds a path to get to a given statement from the “big bang”
Its strategy has to do with making forward and backward entailment cones [?]
With a certain pruning [or is it ordering?]
With a certain pruning [or is it ordering?]
E.g. Knuth-Bendix with a certain ordering only combines certain statements