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"],AspectRatio1/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"],AspectRatio1/2]&/@{"A","AA","AB","BA","BB","AAA","AAB","ABA","ABB","BAA","BAB","BBA","BBB"}

In[]:=

,,,,,,,,,,,,

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: