You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
Expression Transformation Case (i.e. implicational case)
Expression Transformation Case (i.e. implicational case)
[Input is expr + (rule of inference) and this gives ]
In[]:=
AxiomaticTheory["BooleanAxioms"]
Out[]=
a.⊗b.b.⊗a.,a.⊕b.b.⊕a.,a.⊗b.⊕a.,a.⊕b.⊗a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
b.
∀
{a.,b.}
b.
∀
{a.,b.,c.}
∀
{a.,b.,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],#,BackgroundLighter[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],#,BackgroundLighter[Purple,.9]]&)]
Out[]=
Equational Case
Equational Case
Could do it by adding axioms for equality [reflexivity a=a, symmetry a=b, transitivity]
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 ... ]
[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
Minimal axioms
Relation to theorem prover
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....
To emulate theorem prover, can prune items without Equal as head....
Sorting of Boolean algebra
Sorting of Boolean algebra
Simply make the code for an expression always be 0:
[[ overnight runs ]]
[[ overnight runs ]]