WOLFRAM NOTEBOOK

In[]:=
FindEquationalProof[ForAll[x,Implies[Implies[p[x],Implies[q[x],r[x]]],Implies[And[p[x],q[x]],r[x]]]],{}]​​
Out[]=
ProofObject
Logic: Predicate/EquationalLogic
Steps: 115
Theorem:
∀
x
((p[x](q[x]r[x]))(p[x]&&q[x]r[x]))
In[]:=
FindEquationalProof[identity[x],{ForAll[g,Implies[group[g],And[associative[g],ident[g]]]],ForAll[g,Implies[ident[g],And[identity[g],inverse[g]]]],group[x]}]
Out[]=
ProofObject
Logic: Predicate/EquationalLogic
Steps: 98
Theorem: identity[x]
Wolfram Cloud

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 »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.