Boolean Axioms

Not[Not[p]]==p
In[]:=
bax={"BooleanAxioms","HuntingtonAxioms","RobbinsAxioms","ShefferAxioms","HillmanAxioms","MeredithAxioms","OrNotBooleanAxioms","WolframAxioms","WolframAlternateAxioms","WolframCommutativeAxioms"};
In[]:=
#->AxiomaticTheory[#,"Operators"]&/@bax
Out[]=
{BooleanAxiomsAndCircleTimes,OrCirclePlus,NotOverBar,HuntingtonAxiomsOrCirclePlus,NotOverBar,RobbinsAxiomsOrCirclePlus,NotOverBar,ShefferAxiomsNandCenterDot,HillmanAxiomsNandCenterDot,MeredithAxiomsNandCenterDot,OrNotBooleanAxiomsOrCirclePlus,NotOverBar,WolframAxiomsNandCenterDot,WolframAlternateAxiomsNandCenterDot,WolframCommutativeAxiomsNandCenterDot}
In[]:=
Nest[Nand[#,#]&,p,2]/.Nand->CenterDot
Out[]=
(p·p)·(p·p)
In[]:=
#->FindEquationalProof[If[Length[AxiomaticTheory[#,"Operators"]]==1,(p·p)·(p·p)==p,OverBar[OverBar[p]]==p],#]&/@bax
Out[]=
$Aborted
In[]:=
ParallelMap[#->FindEquationalProof[If[Length[AxiomaticTheory[#,"Operators"]]==1,(p·p)·(p·p)==p,OverBar[OverBar[p]]==p],#]&,bax]
Out[]=
$Aborted
In[]:=
ParallelMap[#->FindEquationalProof[If[Length[AxiomaticTheory[#,"Operators"]]==1,(p·p)·(p·p)==p,OverBar[OverBar[p]]==p],#,TimeConstraint->60]&,bax]
Out[]=
BooleanAxiomsProofObject
Logic: EquationalLogic
Steps: 19
Theorem:
p
p
,HuntingtonAxiomsProofObject
Logic: EquationalLogic
Steps: 24
Theorem:
p
p
,RobbinsAxiomsFailure

Message:
No proof could be found within 60 seconds.
Tag:
TimedOut
,ShefferAxiomsProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,HillmanAxiomsProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,MeredithAxiomsProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,OrNotBooleanAxiomsProofObject
Logic: EquationalLogic
Steps: 117
Theorem:
p
p
,WolframAxiomsProofObject
Logic: EquationalLogic
Steps: 54
Theorem: (p·p)·(p·p)p
,WolframAlternateAxiomsProofObject
Logic: EquationalLogic
Steps: 12
Theorem: (p·p)·(p·p)p
,WolframCommutativeAxiomsProofObject
Logic: EquationalLogic
Steps: 8
Theorem: (p·p)·(p·p)p

In[]:=
TextGrid{#1,TraditionalForm[If[Length[AxiomaticTheory[#,"Operators"]]==1,(p·p)·(p·p)==p,OverBar[OverBar[p]]==p]/.{CenterDot->SmallCircle}],Column[TraditionalForm/@(ResourceFunction["UnformalizeSymbols"][Last/@AxiomaticTheory[#1]]/.{CircleTimes->Wedge,CirclePlus->Vee,CenterDot->SmallCircle})],#2["ProofLength"],Rotate[Graph[ProofObjectToTokenEventGraph[#2],VertexLabels->{_->None},ImageSize->{40,Automatic},VertexShapeFunction->Automatic],90Degree]}&@@@"BooleanAxioms"ProofObject
Logic: EquationalLogic
Steps: 19
Theorem:
p
p
,"HuntingtonAxioms"ProofObject
Logic: EquationalLogic
Steps: 24
Theorem:
p
p
,"OrNotBooleanAxioms"ProofObject
Logic: EquationalLogic
Steps: 117
Theorem:
p
p
,"ShefferAxioms"ProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,"HillmanAxioms"ProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,"MeredithAxioms"ProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,"WolframCommutativeAxioms"ProofObject
Logic: EquationalLogic
Steps: 8
Theorem: (p·p)·(p·p)p
,"WolframAxioms"ProofObject
Logic: EquationalLogic
Steps: 54
Theorem: (p·p)·(p·p)p
,"WolframAlternateAxioms"ProofObject
Logic: EquationalLogic
Steps: 12
Theorem: (p·p)·(p·p)p
,Frame->All
Out[]=
BooleanAxioms
p
p
a⋀bb⋀a
a⋀(b⋁c)a⋀b⋁a⋀c
a⋁b⋀
b
a
a⋀(b⋁
b
)a
a⋁bb⋁a
a⋁b⋀c(a⋁b)⋀(a⋁c)
19
HuntingtonAxioms
p
p
a⋁(b⋁c)(a⋁b)⋁c
a⋁bb⋁a
a
⋁b
⋁
a
⋁
b
a
24
OrNotBooleanAxioms
p
p
c⋁b
⋁
a
⋁
d
⋁d
⋁(
a
⋁c)
a
117
ShefferAxioms
(p∘p)∘(p∘p)p
(a∘a)∘(a∘a)a
a∘(b∘(b∘b))a∘a
(a∘(b∘c))∘(a∘(b∘c))((b∘b)∘a)∘((c∘c)∘a)
3
HillmanAxioms
(p∘p)∘(p∘p)p
(a∘a)∘(a∘b)a
a∘(a∘b)a∘(b∘b)
a∘(a∘(b∘c))b∘(b∘(a∘c))
3
MeredithAxioms
(p∘p)∘(p∘p)p
a∘(b∘(a∘c))((c∘b)∘b)∘a
(a∘a)∘(b∘a)a
3
WolframCommutativeAxioms
(p∘p)∘(p∘p)p
a∘bb∘a
(a∘b)∘(a∘(b∘c))a
8
WolframAxioms
(p∘p)∘(p∘p)p
((b∘c)∘a)∘(b∘((b∘a)∘b))a
54
WolframAlternateAxioms
(p∘p)∘(p∘p)p
(a∘((c∘a)∘a))∘(c∘(b∘a))c
12
In[]:=
TextGrid{Column[TraditionalForm/@(ResourceFunction["UnformalizeSymbols"][Last/@AxiomaticTheory[#1]]/.{CircleTimes->Wedge,CirclePlus->Vee,CenterDot->SmallCircle})],TraditionalForm[If[Length[AxiomaticTheory[#,"Operators"]]==1,(p·p)·(p·p)==p,OverBar[OverBar[p]]==p]/.{CenterDot->SmallCircle}],#2["ProofLength"],Rotate[Graph[ProofObjectToTokenEventGraph[#2],VertexLabels->{_->None},ImageSize->{40,Automatic},VertexShapeFunction->Automatic],90Degree]}&@@@"BooleanAxioms"ProofObject
Logic: EquationalLogic
Steps: 19
Theorem:
p
p
,"HuntingtonAxioms"ProofObject
Logic: EquationalLogic
Steps: 24
Theorem:
p
p
,"OrNotBooleanAxioms"ProofObject
Logic: EquationalLogic
Steps: 117
Theorem:
p
p
,"ShefferAxioms"ProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,"HillmanAxioms"ProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,"MeredithAxioms"ProofObject
Logic: EquationalLogic
Steps: 3
Theorem: (p·p)·(p·p)p
,"WolframCommutativeAxioms"ProofObject
Logic: EquationalLogic
Steps: 8
Theorem: (p·p)·(p·p)p
,"WolframAxioms"ProofObject
Logic: EquationalLogic
Steps: 54
Theorem: (p·p)·(p·p)p
,"WolframAlternateAxioms"ProofObject
Logic: EquationalLogic
Steps: 12
Theorem: (p·p)·(p·p)p
,Frame->All
Out[]=
a⋀bb⋀a
a⋀(b⋁c)a⋀b⋁a⋀c
a⋁b⋀
b
a
a⋀(b⋁
b
)a
a⋁bb⋁a
a⋁b⋀c(a⋁b)⋀(a⋁c)
p
p
19
a⋁(b⋁c)(a⋁b)⋁c
a⋁bb⋁a
a
⋁b
⋁
a
⋁
b
a
p
p
24
c⋁b
⋁
a
⋁
d
⋁d
⋁(
a
⋁c)
a
p
p
117
(a∘a)∘(a∘a)a
a∘(b∘(b∘b))a∘a
(a∘(b∘c))∘(a∘(b∘c))((b∘b)∘a)∘((c∘c)∘a)
(p∘p)∘(p∘p)p
3
(a∘a)∘(a∘b)a
a∘(a∘b)a∘(b∘b)
a∘(a∘(b∘c))b∘(b∘(a∘c))
(p∘p)∘(p∘p)p
3
a∘(b∘(a∘c))((c∘b)∘b)∘a
(a∘a)∘(b∘a)a
(p∘p)∘(p∘p)p
3
a∘bb∘a
(a∘b)∘(a∘(b∘c))a
(p∘p)∘(p∘p)p
8
((b∘c)∘a)∘(b∘((b∘a)∘b))a
(p∘p)∘(p∘p)p
54
(a∘((c∘a)∘a))∘(c∘(b∘a))c
(p∘p)∘(p∘p)p
12

Boolean Expressions

Entailment Cone for Notable Theorems

Here should include notable theorems that are axioms

Use WA with translated version of theorems....