You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
Prove modus ponens from equational logic
Prove modus ponens from equational logic
In[]:=
FindEquationalProof[ForAll[x,Implies[a[x],c[x]]],{ForAll[x,Implies[a[x],b[x]]],ForAll[x,Implies[b[x],c[x]]]}]["ProofGraph"]
Out[]=
Equational multiway
Equational multiway
In[]:=
Graph[Rule@@@Last[EquationalMultiwaySystem[{{"AB","BA"},{"AAAB","AAAB"}},6]],VertexLabelsAutomatic]
Out[]=
In[]:=
ResourceFunction["MultiwaySystem"][{"AB""BA","BA""AB"},{"AAAB"},6,"StatesGraph"]
Out[]=
In[]:=
TransitiveClosureGraph[%]
Out[]=
In[]:=
ResourceFunction["FindStringProof"]["AAAB""BAAA",{"AB""BA","BA""AB"}]
Out[]=
ProofObject
In[]:=
%["ProofGraph"]
Out[]=
With{g=%},Graphg,
Out[]=
In[]:=
SimpleGraph[Map[#/.{x_,y_}(x<->y)&,EquationalMultiwaySystem[{{"AB","BA"},{"AAAB","AAAB"}},2,"ProofGraph"],{-2}],VertexLabelsAutomatic];
In[]:=
LayeredGraphPlot[%,("AAAB""AAAB")Top]
Out[]=
This has various multiway branches; the “true proof graph” picks a particular path.
[[ Better to display the rules used with a different edge type from the input edges ]]
DirectedEdge
In[]:=
SimpleGraph[EquationalMultiwaySystem[{{"AB","BA"},{"AAAB","AAAB"}},2,"ProofGraph"],VertexLabels->Automatic,GraphLayout"LayeredDigraphEmbedding",EdgeStyle{DirectedEdge[_,_,1]Gray,DirectedEdge[_,_,2]Dotted}]
Out[]=
Empirical Metamathematics
Empirical Metamathematics
Logic
Logic
Geometry
Geometry
Group theory
Group theory