WOLFRAM NOTEBOOK

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

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
Logic: StringLogic
Steps: 8
Theorem: A(A(AB))B(A(AA))
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

Logic

Geometry

Group theory

Wolfram Cloud

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 »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.