Finding Superaxioms
Finding Superaxioms
[From EdP]
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}]]
In[]:=
Out[]=
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}]]
In[]:=
Out[]=
Total[Length[VertexOutComponent[euc,#]]&/@VertexList[euc]]
In[]:=
25852
Out[]=
[[ Need tradeoff between number of axioms and reduction of this number ]]
ResourceFunction["ParallelMapMonitored"][#(If[!GraphQ[#],0,VertexCount[euc]-VertexCount[#]]&[PruneSubgraph[euc,Subgraph[euc,VertexOutComponent[euc,#]]]])&,VertexList[euc]]
In[]:=
Out[]=
ListLinePlot[%]
In[]:=
$Aborted
Out[]=
ListLinePlot[Values[%%]]
In[]:=
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
With[{g=Subgraph[euc,VertexOutComponent[euc,"Book"1,"Theorem"9,2]]},Graph[g,GraphLayout"LayeredDigraphEmbedding",VertexLabels(#->Placed[EuclidVertexName[#],Center]&/@VertexList[g]),VertexSize.7,VertexStyleLightBlue]]
In[]:=
Out[]=
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}]]
In[]:=
Out[]=
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}]]
In[]:=
Out[]=
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}]]
In[]:=
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....