Relationship to FindEquationalProof
Relationship to FindEquationalProof
In[]:=
NestGraph[Flatten[{Values[coSubstitutionLemmas[#,x_⊕y_y_⊕x_,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,4,GraphLayout->"SpringElectricalEmbedding",VertexLabels->Placed["Name",Tooltip]]
Out[]=
In[]:=
RandomChoiceVertexList
Out[]=
a_⊕((b_⊕c_)⊕(d_⊕(e_⊕f_)))(((f_⊕e_)⊕d_)⊕(c_⊕b_))⊕a_
In[]:=
FindEquationalProof[ForAll[{a,b,c},(a⊕b)⊕c==c⊕(a⊕b)],ForAll[{x,y},x⊕y==y⊕x]]
Out[]=
ProofObject
In[]:=
%["ProofGraph"]
Out[]=
In[]:=
a_⊕((b_⊕c_)⊕(d_⊕(e_⊕f_)))(((f_⊕e_)⊕d_)⊕(c_⊕b_))⊕a_/.p_Pattern:>First[p]
Out[]=
a⊕((b⊕c)⊕(d⊕(e⊕f)))(((f⊕e)⊕d)⊕(c⊕b))⊕a
In[]:=
FindEquationalProof[ForAll[{a,b,c,d,e,f},a⊕((b⊕c)⊕(d⊕(e⊕f)))==(((f⊕e)⊕d)⊕(c⊕b))⊕a],ForAll[{x,y},x⊕y==y⊕x]]
Out[]=
ProofObject
In[]:=
%["ProofGraph"]
Out[]=
In[]:=
%41["ProofDataset"]
Out[]=
In[]:=
Variables[(a⊕b)⊕c==c⊕(b⊕a)]
Out[]=
{}
In[]:=
(ForAll@@{Union[Level[#,{-1}]],#/.TwoWayRule->Equal})&/@VertexList
/.p_Pattern:>First[p]
Out[]=
In[]:=
FindEquationalProof[#,ForAll[{x,y},x⊕y==y⊕x],"ProofGraph"]&/@Take[%,10]
∀
{x,y}
Out[]=
x⊕yy⊕x[ProofGraph],
,
,
,FindEquationalProofTrue,
∀
{x,y}
,
,
,
,
,