# FindEquationalProof

FindEquationalProof[thm,axms]

tries to find a proof of the equational logic theorem thm using the axioms axms.

# Details and Options

• If FindEquationalProof succeeds in reducing the theorem to True using the axioms axms, then it returns a ProofObject expression. If it succeeds in reducing the theorem to False, it returns a Failure object.
• The statements thm and axms can be any logical conjunction of:
•  lhsrhs equational logic identities ForAll[vars,lhsrhs] universal quantifiers over equational logic identities
• FindEquationalProof[expr1&&expr2&&,axm1&&axm2&&] will treat each of expr1,expr2, as a separate hypothesis, and each of axm1,axm2, as a separate axiom.
• FindEquationalProof[{expr1,expr2,},{axm1,axm2,}] is equivalent to FindEquationalProof[expr1&&expr2&&,axm1&&axm2&&].
• FindEquationalProof has the following option:
•  TimeConstraint Infinity how much time to allow
• If FindEquationalProof exceeds the specified time constraint, it returns a Failure object.
• FindEquationalProof[thm,axms] uses the KnuthBendix completion algorithm to prove that the theorem thm follows from the axioms axms.

# Examples

open allclose all

## Basic Examples(2)

Prove an elementary theorem in propositional logic:

 In[1]:=
 Out[1]=

Show the abstract proof network:

 In[2]:=
 Out[2]=

Show the complete list of proof steps as a Dataset object:

 In[3]:=
 Out[3]=

Prove a theorem involving universal quantification in first-order logic:

 In[1]:=
 Out[1]=

Typeset a natural language argument:

 In[2]:=
 Out[2]=

Build a function that performs the steps of the proof:

 In[3]:=
 Out[3]=
 In[4]:=
 Out[4]=