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]],VertexLabelsAutomatic]
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⊙(A⊙B))B⊙(A⊙(A⊙A))

In[]:=
%["ProofGraph"]
Out[]=
With{g=%},Graphg,
SequenceIcon

Out[]=
In[]:=
SimpleGraph[Map[#/.{x_,y_}(x<->y)&,EquationalMultiwaySystem[{{"AB","BA"},{"AAAB","AAAB"}},2,"ProofGraph"],{-2}],VertexLabelsAutomatic];
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