You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
In[]:=
stheorems=a.a.⋀a.,a.a.⋁a.,a.⋀b.b.⋀a.,a.⋁b.b.⋁a.,a.a.,a.a.⋀(a.⋁b.),a.a.⋁a.⋀b.,a.⋀a.b.⋀b.,a.⋁a.b.⋁b.,a.⋀b.a.⋀(a.⋀b.),(a.⋀b.)⋀c.a.⋀(b.⋀c.),(a.⋁b.)⋁c.a.⋁(b.⋁c.),a.⋁b.⋀c.(a.⋁b.)⋀(a.⋁c.),a.⋀(b.⋁c.)a.⋀b.⋁a.⋀c.,(a.⋁b.)a.⋀b.,(a.⋀b.)a.⋁b.,a.a.⋁b.⋀b.,a.a.⋀(b.⋁b.),a.⋁b.a.⋁a.⋀b.,a.⋁b.b.⋁a.;
∀
a.
∀
a.
∀
{a.,b.}
∀
{a.,b.}
∀
a.
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
In[]:=
toProve=(Delete[#,0]&/@stheorems)[[2;;;;2]]
Out[]=
{a.a.⋀a.,a.a.⋁a.,a.⋀b.b.⋀a.,a.⋁b.b.⋁a.,a.a.,a.a.⋀(a.⋁b.),a.a.⋁a.⋀b.,a.⋀a.b.⋀b.,a.⋁a.b.⋁b.,a.⋀b.a.⋀(a.⋀b.),(a.⋀b.)⋀c.a.⋀(b.⋀c.),(a.⋁b.)⋁c.a.⋁(b.⋁c.),a.⋁b.⋀c.(a.⋁b.)⋀(a.⋁c.),a.⋀(b.⋁c.)a.⋀b.⋁a.⋀c.,(a.⋁b.)a.⋀b.,(a.⋀b.)a.⋁b.,a.a.⋁b.⋀b.,a.a.⋀(b.⋁b.),a.⋁b.a.⋁a.⋀b.,a.⋁b.b.⋁a.}
In[]:=
nntheorems=toProve//.{Square[a._]->a.·a.,Wedge[a._,b._]->(a.·b.)·(a.·b.),Vee[a._,b._]->(a.·a.)·(b.·b.)}
Out[]=
{a.(a.·a.)·(a.·a.),a.(a.·a.)·(a.·a.),(a.·b.)·(a.·b.)(b.·a.)·(b.·a.),(a.·a.)·(b.·b.)(b.·b.)·(a.·a.),(a.·a.)·(a.·a.)a.,a.(a.·((a.·a.)·(b.·b.)))·(a.·((a.·a.)·(b.·b.))),a.(a.·a.)·(((a.·b.)·(a.·b.))·((a.·b.)·(a.·b.))),((a.·a.)·a.)·((a.·a.)·a.)((b.·b.)·b.)·((b.·b.)·b.),((a.·a.)·(a.·a.))·(a.·a.)((b.·b.)·(b.·b.))·(b.·b.),(a.·b.)·(a.·b.)(a.·((a.·b.)·(a.·b.)))·(a.·((a.·b.)·(a.·b.))),(((a.·b.)·(a.·b.))·c.)·(((a.·b.)·(a.·b.))·c.)(a.·((b.·c.)·(b.·c.)))·(a.·((b.·c.)·(b.·c.))),(((a.·a.)·(b.·b.))·((a.·a.)·(b.·b.)))·(c.·c.)(a.·a.)·(((b.·b.)·(c.·c.))·((b.·b.)·(c.·c.))),(a.·a.)·(((b.·c.)·(b.·c.))·((b.·c.)·(b.·c.)))(((a.·a.)·(b.·b.))·((a.·a.)·(c.·c.)))·(((a.·a.)·(b.·b.))·((a.·a.)·(c.·c.))),(a.·((b.·b.)·(c.·c.)))·(a.·((b.·b.)·(c.·c.)))(((a.·b.)·(a.·b.))·((a.·b.)·(a.·b.)))·(((a.·c.)·(a.·c.))·((a.·c.)·(a.·c.))),True,((a.·b.)·(a.·b.))·((a.·b.)·(a.·b.))((a.·a.)·(a.·a.))·((b.·b.)·(b.·b.)),a.(a.·a.)·(((b.·(b.·b.))·(b.·(b.·b.)))·((b.·(b.·b.))·(b.·(b.·b.)))),a.(a.·((b.·b.)·((b.·b.)·(b.·b.))))·(a.·((b.·b.)·((b.·b.)·(b.·b.)))),(a.·a.)·(b.·b.)(a.·a.)·((((a.·a.)·b.)·((a.·a.)·b.))·(((a.·a.)·b.)·((a.·a.)·b.))),((a.·a.)·(a.·a.))·(b.·b.)(((b.·b.)·(b.·b.))·((b.·b.)·(b.·b.)))·((a.·a.)·(a.·a.))}
In[]:=
Position[%,True]
Out[]=
{{15}}
In[]:=
toProve[[15]]
Out[]=
(a.⋁b.)a.⋀b.
In[]:=
FindEquationalProof[First[nntheorems],AxiomaticTheory["WolframAxioms"]]
Out[]=
ProofObject
In[]:=
ResourceFunction["ParallelMapMonitored"][FindEquationalProof[#,AxiomaticTheory["WolframAxioms"]]&,nntheorems]
(kernel 77)
FindEquationalProof::invs:Invalid specification of propositions True and axioms ((b.·c.)·a.)·(b.·((b.·a.)·b.))a..
∀
{a.,b.,c.}
∀
{a.,b.,c.}
Out[]=
In[]:=
#["ProofLength"]&/@%
Out[]=
54,54,103,102,54,95,92,132,143,91,328,274,958,1502,FindEquationalProofTrue,((b.·c.)·a.)·(b.·((b.·a.)·b.))a.[ProofLength],56,131,130,120,103
∀
{a.,b.,c.}