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:
  • lhsrhsequational logic identities
    ForAll[vars,lhsrhs]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:
  • TimeConstraintInfinityhow 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]:=
Click for copyable input
Out[1]=

Show the abstract proof network:

In[2]:=
Click for copyable input
Out[2]=

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

In[3]:=
Click for copyable input
Out[3]=

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

In[1]:=
Click for copyable input
Out[1]=

Typeset a natural language argument:

In[2]:=
Click for copyable input
Out[2]=

Build a function that performs the steps of the proof:

In[3]:=
Click for copyable input
Out[3]=
In[4]:=
Click for copyable input
Out[4]=

Scope  (2)

Options  (1)

Applications  (8)

Properties & Relations  (2)

Possible Issues  (1)

See Also

ProofObject  FullSimplify  Reduce  FindInstance

Introduced in 2018
(11.3)