In[]:=
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"}
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
In[]:=
FindStringReplacePath[{"B""ABA","AA""B","BB""A"},"B",#]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
Out[]=
{{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}}
In[]:=
LayeredGraphPlot[FindStringReplacePath[{"B""ABA","AA""B","BB""A"},"B",#,"MultiwayFragment"],AspectRatio1/2]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
In[]:=
FindStringReplacePath[{"B""ABA","AA""B","BB""A"},"B","A","MultiwayFragment"]
Out[]=
In[]:=
FindStringReplacePath[{"B"->"ABA","AA"->"B","BB"->"A"},"B",#]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
Out[]=
{{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}}
In[]:=
LayeredGraphPlot[FindStringReplacePath[{"B"->"ABA","AA"->"B","BB"->"A"},"B",#,"MultiwayFragment"],AspectRatio1/2]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
Also want to include causal edges....
Also want to include causal edges....
Proof Shortening
Proof Shortening
Equational Theorem Proving
Equational Theorem Proving
Undirected graph. Ask if one can reach the “True” state...
Completion-based theorem proving...
This generates A==A
Equational vs. Transformational
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
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”
Graph Neighboring / “Plumbing”
Models / Foliations
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
Adding Relations
Does adding relations lead to termination?
Add relations based on a certain path ... what then happens?
Add relations based on a certain path ... what then happens?
No difference if only one step anyway: