Finding Superaxioms
Finding Superaxioms
[From EdP]
In[]:=
PruneSubgraph[graph_,subgraph_]:=Module[{subBranches,branches,prunecheck,prunable},subBranches=Sort[Tally[Last/@Union[EdgeList[subgraph]]]];branches=Tally[Last/@Union[EdgeList[graph]]];prunecheck=Sort[Select[branches,MemberQ[First/@subBranches,#[[1]]]&]];prunable=Table[If[prunecheck[[n,2]]==subBranches[[n,2]],prunecheck[[n,1]],Sequence@@{}],{n,1,Length[prunecheck]}];If[Length[prunable]0,"Same graph",Graph[Select[EdgeList[graph],Not[MemberQ[prunable,First[#]]]&]]]]
In[]:=
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"12]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"9|>Red}]]
Out[]=
In[]:=
With[{g=PruneSubgraph[Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"12]],Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9]]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"9|>Red}]]
Out[]=
In[]:=
Total[Length[VertexOutComponent[euc,#]]&/@VertexList[euc]]
Out[]=
25852
[[ Need tradeoff between number of axioms and reduction of this number ]]
In[]:=
ResourceFunction["ParallelMapMonitored"][#(If[!GraphQ[#],0,VertexCount[euc]-VertexCount[#]]&[PruneSubgraph[euc,Subgraph[euc,VertexOutComponent[euc,#]]]])&,VertexList[euc]]
Out[]=
In[]:=
ListLinePlot[%]
Out[]=
$Aborted
In[]:=
ListLinePlot[Values[%%]]
Out[]=
The above seems to be WRONG...
The above seems to be WRONG...
Instead, for any given theorem, stop if one reaches the superaxiom before the axioms
Instead, for any given theorem, stop if one reaches the superaxiom before the axioms
In[]:=
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9,2]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyleLightBlue]]
Out[]=
In[]:=
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9,2]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"2|>Red}]]
Out[]=
In[]:=
With[{g=GraphDifference[Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9,2]],Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"2,2]]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"2|>Red}]]
Out[]=
In[]:=
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"2,"Theorem"9,2]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyle{_->LightBlue,<|"Book"1,"Theorem"2|>Red}]]
Out[]=
Another Definition
Another Definition
[[ Need tradeoff between number of axioms and reduction of this number ]]
Does the wrong thing for lower-numbered theorems....
Does the wrong thing for lower-numbered theorems....