Expression Transformation Case (i.e. implicational case)

[Input is expr + (rule of inference) and this gives ]
In[]:=
AxiomaticTheory["BooleanAxioms"]
Out[]=

∀
{a.,b.}
a.⊗b.b.⊗a.,
∀
{a.,b.}
a.⊕b.b.⊕a.,
∀
{a.,b.}
a.⊗b.⊕
b.
a.,
∀
{a.,b.}
a.⊕b.⊗
b.
a.,
∀
{a.,b.,c.}
a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,
∀
{a.,b.,c.}
a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
In[]:=
ResourceFunction["MultiwayOperatorSystem"][{And[a_,b_]And[b,a],Or[a_,b_]Or[b,a],And[a_,Or[b_,Not[b_]]]a,Or[a_,And[b_,Not[b_]]]a,a_Module[{b=Unique[]},And[a,Or[b,Not[b]]]],a_Module[{b=Unique[]},Or[a,And[b,Not[b]]]],And[a_,Or[b_,c_]]Or[And[a,b],And[a,c]],Or[And[a_,b_],And[a_,c_]]And[a,Or[b,c]],Or[a_,And[b_,c_]]And[Or[a,b],Or[a,c]],And[Or[a_,b_],Or[a_,c_]]Or[a,And[b,c]]},And[x,y],2,"StatesGraphStructure"]
Out[]=
In[]:=
ResourceFunction["MultiwayOperatorSystem"][{And[a_,b_]And[b,a],Or[a_,b_]Or[b,a],And[a_,Or[b_,Not[b_]]]a,Or[a_,And[b_,Not[b_]]]a,a_Module[{b},And[a,Or[b,Not[b]]]],a_Module[{b},Or[a,And[b,Not[b]]]],And[a_,Or[b_,c_]]Or[And[a,b],And[a,c]],Or[And[a_,b_],And[a_,c_]]And[a,Or[b,c]],Or[a_,And[b_,c_]]And[Or[a,b],Or[a,c]],And[Or[a_,b_],Or[a_,c_]]Or[a,And[b,c]]},And[x,y],2,"StatesGraph"]
Out[]=
In[]:=
BooleanDisplay[expr_]:=With[{symbs=Union[Level[expr,{-1}]]},expr/.Thread[(#Take[Alphabet["Greek"],Length[#]])&[Select[symbs,StringContainsQ[SymbolName[#],"$"]&]]]]
In[]:=
Graph[ResourceFunction["MultiwayOperatorSystem"][{And[a_,b_]And[b,a],Or[a_,b_]Or[b,a],And[a_,Or[b_,Not[b_]]]a,Or[a_,And[b_,Not[b_]]]a,a_Module[{b},And[a,Or[b,Not[b]]]],a_Module[{b},Or[a,And[b,Not[b]]]],And[a_,Or[b_,c_]]Or[And[a,b],And[a,c]],Or[And[a_,b_],And[a_,c_]]And[a,Or[b,c]],Or[a_,And[b_,c_]]And[Or[a,b],Or[a,c]],And[Or[a_,b_],Or[a_,c_]]Or[a,And[b,c]]},And[x,y],1,"StatesGraph","StateRenderingFunction"(Inset[Style[TraditionalForm[BooleanDisplay[ToExpression[#2]]],Black],#,BackgroundLighter[Purple,.9]]&)],GraphLayout"SpringElectricalEmbedding"]
Out[]=
In[]:=
ResourceFunction["MultiwayOperatorSystem"][{And[a_,b_]And[b,a],Or[a_,b_]Or[b,a],And[a_,Or[b_,Not[b_]]]a,Or[a_,And[b_,Not[b_]]]a,a_Module[{b},And[a,Or[b,Not[b]]]],a_Module[{b},Or[a,And[b,Not[b]]]],And[a_,Or[b_,c_]]Or[And[a,b],And[a,c]],Or[And[a_,b_],And[a_,c_]]And[a,Or[b,c]],Or[a_,And[b_,c_]]And[Or[a,b],Or[a,c]],And[Or[a_,b_],Or[a_,c_]]Or[a,And[b,c]]},And[x,y],2,"StatesGraph","StateRenderingFunction"(Inset[Style[TraditionalForm[BooleanDisplay[ToExpression[#2]]],Black],#,BackgroundLighter[Purple,.9]]&)]
Out[]=

Equational Case

Could do it by adding axioms for equality [reflexivity a=a, symmetry a=b, transitivity]

Now the transformation rules and the expressions are of the same form.
​
[We could do this with expressions that are implications ... ]
Need a version of True that is held.....
[[[ Overbar is probably failing in stringificaiton ]]]

Minimal axioms

Relation to theorem prover

Substitution lemmas find a path through this graph
[ Nontrivial assumption: equality that appears inside the states is the same as the equality in the rules ]
Completion is:
To create this critical pair lemma, need to drill inside to look at expressions
[ But need a common expression (subpattern) to which to apply the rules ]

To emulate theorem prover, can prune items without Equal as head....

Sorting of Boolean algebra

Simply make the code for an expression always be 0:

[[ overnight runs ]]