In[]:=
geometry={ForAll[{x,y,z},implies[congruent[line[x,y],line[z,z]],congruent[x,y]]],ForAll[{x,y,z,u,v,w},implies[and[congruent[line[x,y],line[z,u]],congruent[line[x,y],line[v,w]]],congruent[line[z,u],line[v,w]]]],ForAll[{x,y,z},implies[between[x,y,z],equal[x,y]]],ForAll[{x,y,z,u,v},implies[and[between[x,u,z],between[y,v,z]],Exists[a,and[between[u,a,y],between[v,a,x]]]]],ForAll[{x,y,z,u,v},implies[and[and[and[congruent[line[x,u],line[x,v]],congruent[line[y,u],line[y,v]]],congruent[line[z,u],line[z,v]]],not[equal[u,v]]],or[or[between[x,y,z],between[y,z,x]],between[z,x,y]]]],ForAll[{x,y,z,u,v,w},implies[and[and[and[between[x,y,w],congruent[line[x,y],line[y,w]]],and[between[x,u,v],congruent[line[x,u],line[u,v]]]],and[between[y,u,z],congruent[line[y,u],line[z,u]]]],congruent[line[y,z],line[v,w]]]],ForAll[{x,y,z,a,b,c,u,v},implies[and[and[and[and[and[and[not[equal[x,y]],between[x,y,z]],between[a,b,c]],congruent[line[x,y],line[a,b]]],congruent[line[y,z],line[b,c]]],congruent[line[x,u],line[a,v]]],congruent[line[y,u],line[b,v]]],congruent[line[z,u],line[c,v]]]],ForAll[{x,y},implies[equal[x,y],equal[y,x]]],ForAll[{x,y,z},implies[and[equal[x,y],equal[y,z]],equal[x,z]]],ForAll[x,equal[x,x]],ForAll[{a,b},and[a,b]and[b,a]],ForAll[{a,b},or[a,b]or[b,a]],ForAll[{a,b},and[a,or[b,not[b]]]a],ForAll[{a,b},or[a,and[b,not[b]]]a],ForAll[{a,b,c},and[a,or[b,c]]or[and[a,b],and[a,c]]],ForAll[{a,b,c},or[a,and[b,c]]and[or[a,b],or[a,c]]],ForAll[{a,b},implies[a,b]or[not[a],b]],HoldForm[ForAll[{α,β,y,z},implies[Exists[x,implies[and[α[y],β[z]],between[x,y,z]]],Exists[u,implies[and[α[y],β[z]],between[y,u,z]]]]]]};
In[]:=
Last/@%
Out[]=
implies[congruent[line[x,y],line[z,z]],congruent[x,y]],implies[and[congruent[line[x,y],line[z,u]],congruent[line[x,y],line[v,w]]],congruent[line[z,u],line[v,w]]],implies[between[x,y,z],equal[x,y]],implies[and[between[x,u,z],between[y,v,z]],and[between[u,a,y],between[v,a,x]]],implies[and[and[and[congruent[line[x,u],line[x,v]],congruent[line[y,u],line[y,v]]],congruent[line[z,u],line[z,v]]],not[equal[u,v]]],or[or[between[x,y,z],between[y,z,x]],between[z,x,y]]],implies[and[and[and[between[x,y,w],congruent[line[x,y],line[y,w]]],and[between[x,u,v],congruent[line[x,u],line[u,v]]]],and[between[y,u,z],congruent[line[y,u],line[z,u]]]],congruent[line[y,z],line[v,w]]],implies[and[and[and[and[and[and[not[equal[x,y]],between[x,y,z]],between[a,b,c]],congruent[line[x,y],line[a,b]]],congruent[line[y,z],line[b,c]]],congruent[line[x,u],line[a,v]]],congruent[line[y,u],line[b,v]]],congruent[line[z,u],line[c,v]]],implies[equal[x,y],equal[y,x]],implies[and[equal[x,y],equal[y,z]],equal[x,z]],equal[x,x],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,and[a,or[b,c]]or[and[a,b],and[a,c]],or[a,and[b,c]]and[or[a,b],or[a,c]],implies[a,b]or[not[a],b],implies[implies[and[α[y],β[z]],between[x,y,z]],implies[and[α[y],β[z]],between[y,u,z]]]
∃
a
∀
{y,z}
∃
x
∃
u
In[]:=
ResourceFunction["FindHeadArities"]@@{%295}
Out[]=
and{2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2},between{3,3,3,3,3,3,3,3,3,3,3,3,3,3,3},congruent{2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2},equal{2,2,2,2,2,2,2,2,2},Equal{2,2,2,2,2,2,2},Exists{2,2,2},ForAll{2},implies{2,2,2,2,2,2,2,2,2,2,2,2,2},line{2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2},List{2,18},not{1,1,1,1,1},or{2,2,2,2,2,2,2,2,2,2,2,2},α{1,1},β{1,1}
In[]:=
First/@%
Out[]=
and2,between3,congruent2,equal2,Equal2,Exists2,ForAll2,implies2,line2,List2,not1,or2,α1,β1
In[]:=
Groupings[{a,b,a},{between3,congruent2,implies2,line2}]
Out[]=
{between[a,b,a],congruent[congruent[a,b],a],congruent[a,congruent[b,a]],congruent[implies[a,b],a],congruent[a,implies[b,a]],implies[congruent[a,b],a],implies[a,congruent[b,a]],congruent[line[a,b],a],congruent[a,line[b,a]],line[congruent[a,b],a],line[a,congruent[b,a]],implies[implies[a,b],a],implies[a,implies[b,a]],implies[line[a,b],a],implies[a,line[b,a]],line[implies[a,b],a],line[a,implies[b,a]],line[line[a,b],a],line[a,line[b,a]]}
In[]:=
Most[geometry]
Out[]=
implies[congruent[line[x,y],line[z,z]],congruent[x,y]],implies[and[congruent[line[x,y],line[z,u]],congruent[line[x,y],line[v,w]]],congruent[line[z,u],line[v,w]]],implies[between[x,y,z],equal[x,y]],implies[and[between[x,u,z],between[y,v,z]],and[between[u,a,y],between[v,a,x]]],implies[and[and[and[congruent[line[x,u],line[x,v]],congruent[line[y,u],line[y,v]]],congruent[line[z,u],line[z,v]]],not[equal[u,v]]],or[or[between[x,y,z],between[y,z,x]],between[z,x,y]]],implies[and[and[and[between[x,y,w],congruent[line[x,y],line[y,w]]],and[between[x,u,v],congruent[line[x,u],line[u,v]]]],and[between[y,u,z],congruent[line[y,u],line[z,u]]]],congruent[line[y,z],line[v,w]]],implies[and[and[and[and[and[and[not[equal[x,y]],between[x,y,z]],between[a,b,c]],congruent[line[x,y],line[a,b]]],congruent[line[y,z],line[b,c]]],congruent[line[x,u],line[a,v]]],congruent[line[y,u],line[b,v]]],congruent[line[z,u],line[c,v]]],implies[equal[x,y],equal[y,x]],implies[and[equal[x,y],equal[y,z]],equal[x,z]],equal[x,x],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,and[a,or[b,c]]or[and[a,b],and[a,c]],or[a,and[b,c]]and[or[a,b],or[a,c]],implies[a,b]or[not[a],b]
∀
{x,y,z}
∀
{x,y,z,u,v,w}
∀
{x,y,z}
∀
{x,y,z,u,v}
∃
a
∀
{x,y,z,u,v}
∀
{x,y,z,u,v,w}
∀
{x,y,z,a,b,c,u,v}
∀
{x,y}
∀
{x,y,z}
∀
x
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b,c}
∀
{a,b,c}
∀
{a,b}
In[]:=
FindEquationalProof[#,Most[geometry]]&/@%299
Out[]=
$Aborted
In[]:=
FindEquationalProof[congruent[congruent[a,b],a],Most[geometry]]
Out[]=
$Aborted
Assume things, then prove more....
Assume things, then prove more....
In[]:=
all43=Take[Select[FindAllAON[4,3],LowestQ[#,{a,b,c}]&],150]
Out[]=
{ab,aa,ab,ab,aa⋀a,aa⋀a,aa⋁a,aa⋁a,a⋀aa⋁a,aa⋀b,aa⋀b,a⋀aa⋀b,a⋁aa⋀b,aa⋁b,aa⋁b,a⋀aa⋁b,a⋁aa⋁b,a⋀ba⋁b,a⋀ba⋀c,a⋁ba⋀c,a⋀ba⋁c,a⋁ba⋁c,ab⋀a,ab⋀a,a⋀ab⋀a,a⋁ab⋀a,a⋀bb⋀a,a⋁bb⋀a,ab⋁a,ab⋁a,a⋀ab⋁a,a⋁ab⋁a,a⋀bb⋁a,a⋁bb⋁a,ab⋀b,ab⋀b,a⋀ab⋀b,a⋁ab⋀b,a⋀bb⋀b,a⋁bb⋀b,ab⋁b,ab⋁b,a⋀ab⋁b,a⋁ab⋁b,a⋀bb⋁b,a⋁bb⋁b,ab⋀c,ab⋀c,a⋀ab⋀c,a⋁ab⋀c,a⋀bb⋀c,a⋁bb⋀c,ab⋁c,ab⋁c,a⋀ab⋁c,a⋁ab⋁c,a⋀bb⋁c,a⋁bb⋁c,a⋀bc⋀a,a⋁bc⋀a,a⋀bc⋁a,a⋁bc⋁a,a⋀bc⋀b,a⋁bc⋀b,a⋀bc⋁b,a⋁bc⋁b,a⋀bc⋀c,a⋁bc⋀c,a⋀bc⋁c,a⋁bc⋁c,aa,aa,a⋀aa,a⋁aa,a⋀ba,a⋁ba,ab,ab,a⋀ab,a⋁ab,a⋀bb,a⋁bb,ab,a⋀bc,a⋁bc,aa⋀a,aa⋀a,a⋀aa⋀a,a⋁aa⋀a,a⋀ba⋀a,a⋁ba⋀a,aa⋀a,aa⋀a,aa⋀a,a⋀aa⋀a,a⋁aa⋀a,a⋀ba⋀a,a⋁ba⋀a,aa⋀a,a⋀aa⋀a,aa⋁a,aa⋁a,a⋀aa⋁a,a⋁aa⋁a,a⋀ba⋁a,a⋁ba⋁a,aa⋁a,a⋀aa⋁a,a⋀aa⋁a,aa⋁a,aa⋁a,a⋀aa⋁a,a⋁aa⋁a,a⋀ba⋁a,a⋁ba⋁a,aa⋁a,a⋀aa⋁a,a⋀aa⋁a,a⋁aa⋁a,a(a⋀a),a(a⋀a),a⋀a(a⋀a),a⋁a(a⋀a),a⋀b(a⋀a),a⋁b(a⋀a),a(a⋀a),a⋀a(a⋀a),a⋀a(a⋀a),a⋁a(a⋀a),a⋁a(a⋀a),a(a⋁a),a(a⋁a),a⋀a(a⋁a),a⋁a(a⋁a),a⋀b(a⋁a),a⋁b(a⋁a),a(a⋁a),a⋀a(a⋁a),a⋀a(a⋁a),a⋁a(a⋁a),a⋁a(a⋁a),(a⋀a)(a⋁a),aa⋀b,aa⋀b,a⋀aa⋀b,a⋁aa⋀b,a⋀ba⋀b,a⋁ba⋀b,aa⋀b,a⋀aa⋀b}
FindEquationalProof[a⋁ab⋀b,Append[
In[]:=
BooleanTable[a⋀ba⋀a/.{VeeOr,WedgeAnd,SquareNot},{a,b}]
Out[]=
{False,True,True,True}
In[]:=
SatisfiabilityInstances[a⋀ba⋀a/.{VeeOr,WedgeAnd,SquareNot},{a,b}]
Out[]=
{{True,False}}
In[]:=
SatisfiabilityInstances[aa/.{VeeOr,WedgeAnd,SquareNot},{a,b}]
Out[]=
{}
In[]:=
a43=Cases[Take[Select[FindAllAON[4,3],LowestQ[#,{a,b,c}]&],150]/.{VeeOr,WedgeAnd,SquareNot},_Equal]
Out[]=
In[]:=
FindSats[expr_]:=With[{vars=Union[Level[expr,{-1}]]},Thread/@(vars#&/@SatisfiabilityInstances[expr,vars,All])]
In[]:=
FindSats/@Take[a43,15]
Out[]=
{{{aTrue,bTrue},{aFalse,bFalse}},{},{{aTrue,bFalse},{aFalse,bTrue}},{{aTrue,bTrue},{aFalse,bFalse}},{{aTrue},{aFalse}},{},{{aTrue},{aFalse}},{},{{aTrue},{aFalse}},{{aTrue,bTrue},{aFalse,bTrue},{aFalse,bFalse}},{{aTrue,bFalse}},{{aTrue,bTrue},{aFalse,bTrue},{aFalse,bFalse}},{{aTrue,bTrue},{aFalse,bTrue},{aFalse,bFalse}},{{aTrue,bTrue},{aTrue,bFalse},{aFalse,bFalse}},{{aFalse,bTrue}}}
In[]:=
a43r=FindSats/@a43;
In[]:=
CheckTrue[expr_,reps_]:=TrueQ[Length[reps]>0&&AllTrue[reps,expr/.#&]]
In[]:=
Outer[CheckTrue,a43,a43r,1]
Out[]=
In[]:=
ArrayPlot[Boole[%]]
Out[]=
Proof from minimal axiom
Proof from minimal axiom