With[{g=ResourceFunction["FindStringProof"]["B"#,{"B""ABA","AA""B","BB""A"}]["ProofGraph"]},Graph[g,VertexSize.1,VertexLabels(#[[1]]Placed[(#[[2,1,2,1,2]]//.CircleDot[a_,b_]Row[{a,b}]),Center]&/@Options[g,"AnnotationRules"][[1,2]])]]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
In[]:=

,
,
,
,
,
,
,
,
,
,
,
,

Out[]=
FindStringReplacePath[{"B""ABA","AA""B","BB""A"},"B",#]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
In[]:=
{{B,ABA,AAAA,AAB,BB,A},{B,AA},{B,AA,BBA,AABA,AB},{B,AA,ABB,ABAA,BA},{B,ABA,AAAA,AAB,BB},{B,ABA,AABAA,AABB,AAA},{B,ABA,AAAA,AAB},{B,ABA},{B,AA,ABB},{B,ABA,AAAA,BAA},{B,AA,ABB,AAAB,BAB},{B,AA,BBA},{B,ABA,AABAA,AABB,BBB}}
Out[]=
LayeredGraphPlot[FindStringReplacePath[{"B""ABA","AA""B","BB""A"},"B",#,"MultiwayFragment"],AspectRatio1/2]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
In[]:=

,
,
,
,
,
,
,
,
,
,
,
,

Out[]=
FindStringReplacePath[{"B""ABA","AA""B","BB""A"},"B","A","MultiwayFragment"]
In[]:=
Out[]=
FindStringReplacePath[{"B"->"ABA","AA"->"B","BB"->"A"},"B",#]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
In[]:=
{{B,ABA,AABAA,AAABAAA,AAAABAAAA,AAAABBAA,AAAAAAA,AAAAAB,AAABB,AAAA,AAB,BB,A},{B,ABA,AABAA,AABB,AAA,AB,AABA,BBA,AA},{B,ABA,AABAA,AABB,AAA,AB},{B,ABA,AABAA,AABB,AAA,BA},{B,ABA,AABAA,AAABAAA,AAABBA,AAAAA,AAAB,AAAABA,AABBA,AAAA,AAB,BB},{B,ABA,AABAA,AABB,AAA},{B,ABA,AABAA,AAABAAA,AAABBA,AAAAA,AAAB,AAAABA,AABBA,AAAA,AAB},{B,ABA},{B,ABA,AABAA,AABB,AAA,BA,ABAA,ABB},{B,ABA,AABAA,AAABAAA,AAABBA,AAAAA,AAAB,AAAABA,AABBA,AAAA,BAA},{B,ABA,AABAA,AAABAAA,AAABAB,ABBAB,AAAB,BAB},{B,ABA,AABAA,AABB,AAA,AB,AABA,BBA},{B,ABA,AABAA,AABB,BBB}}
Out[]=
LayeredGraphPlot[FindStringReplacePath[{"B"->"ABA","AA"->"B","BB"->"A"},"B",#,"MultiwayFragment"],AspectRatio1/2]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
In[]:=

,
,
,
,
,
,
,
,
,
,
,
,

Out[]=

Also want to include causal edges....

Proof Shortening

Equational Theorem Proving

Undirected graph. Ask if one can reach the “True” state...
Completion-based theorem proving...
This generates A==A

Equational vs. Transformational

x == y can be transformed to f[x] == y where x == f[x]

There are only branch pairs if LHSs can overlap

In the case above, all results used come directly from the original axioms

Graph Neighboring / “Plumbing”

Models / Foliations

What comes before what?
Can we read off possible theorems just by knowing “coordinate values” of the two strings?
Completions vs. foliations etc.

Adding Relations

Does adding relations lead to termination?

Add relations based on a certain path ... what then happens?

No difference if only one step anyway: