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[]:=
AxiomaticTheory["ShefferAxioms"]
Out[]=
(a.·a.)·(a.·a.)a.,a.·(b.·(b.·b.))a.·a.,(a.·(b.·c.))·(a.·(b.·c.))((b.·b.)·a.)·((c.·c.)·a.)
∀
a.
∀
{a.,b.}
∀
{a.,b.,c.}
In[]:=
AxiomaticTheory[]
Out[]=
{AbelianGroupAxioms,AbelianMcCuneAxioms,AbelianTarskiAxioms,BooleanAxioms,CentralGroupoidAxioms,CombinatorAxioms,CommutativeRingAxioms,CommutativeRingWithIdentityAxioms,EquivalentialCalculusAxioms,FieldAxioms,GroupAxioms,HigmanNeumannAxioms,HillmanAxioms,HuntingtonAxioms,ImplicationalCalculusAxioms,JunctionalCalculusAxioms,LeftNearRingAxioms,McCuneAxioms,MeadowAxioms,MeredithAxioms,MonoidAxioms,OrNotBooleanAxioms,RightNearRingAxioms,RingAxioms,RingWithIdentityAxioms,RobbinsAxioms,SemigroupAxioms,SemiringAxioms,ShefferAxioms,SquagAxioms,WolframAlternateAxioms,WolframAxioms,WolframCommutativeAxioms}
In[]:=
AxiomaticTheory["HillmanAxioms"]
Out[]=
(a.·a.)·(a.·b.)a.,a.·(a.·b.)a.·(b.·b.),a.·(a.·(b.·c.))b.·(b.·(a.·c.))
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.,c.}
In[]:=
AxiomaticTheory["MeredithAxioms"]
Out[]=
a.·(b.·(a.·c.))((c.·b.)·b.)·a.,(a.·a.)·(b.·a.)a.
∀
{a.,b.,c.}
∀
{a.,b.}
In[]:=
AxiomaticTheory["WolframAlternateAxioms"]
Out[]=
(a.·((c.·a.)·a.))·(c.·(b.·a.))c.
∀
{a.,b.,c.}
In[]:=
AxiomaticTheory["WolframCommutativeAxioms"]
Out[]=
a.·b.b.·a.,(a.·b.)·(a.·(b.·c.))a.
∀
{a.,b.}
∀
{a.,b.,c.}
In[]:=
AxiomaticTheory["BooleanAxioms"]
Out[]=
a.⊗b.b.⊗a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗a.,a.⊗b.⊕a.,a.⊕b.b.⊕a.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.}
b.
∀
{a.,b.}
b.
∀
{a.,b.}
∀
{a.,b.,c.}
In[]:=
FindEquationalProof[(a.·((c.·a.)·a.))·(c.·(b.·a.))c.,"WolframAxioms"]
Out[]=
ProofObject
In[]:=
FindEquationalProof[(a.·((c.·a.)·a.))·(c.·(b.·a.))c.,"WolframCommutativeAxioms"]
Out[]=
ProofObject
In[]:=
ProofGraph[%74]
Out[]=
In[]:=
ProofGraph[%74,"TokenLabeling"->True]
Out[]=
In[]:=
Clear[ReverseProofGraph]
In[]:=
ReverseProofGraph[FindEquationalProof[(a.·((c.·a.)·a.))·(c.·(b.·a.))c.,"WolframCommutativeAxioms"]]
Out[]=
In[]:=
ReverseProofGraph@Once@FindEquationalProof[{p·q==q·p,(p·p)·(p·p)==p},AxiomaticTheory["WolframAxioms"]]
Out[]=
Waldmeister Options
Waldmeister Options
Proof Display
Proof Display
Proof Step
Proof Step
Same thing, but with different names: