ProofObject

ProofObject[]

represents a proof object generated by FindEquationalProof.

Details

  • Properties of a proof can be obtained using ProofObject[]["prop"].
  • Possible properties include:
  • "ProofDataset"proof steps as a dataset
    "ProofGraph"abstract proof network
    "ProofNotebook"proof written out in a notebook
    "ProofFunction"function for validating rewrite rules
    "Theorem"statement of theorem
    "Axioms"statement of axioms
    "Logic"type of logic used (e.g. "EquationalLogic")

Examples

open allclose all

Basic Examples  (1)

Prove a theorem in first-order logic:

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

Show the theorem statement:

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

State the axioms of the theorem:

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

Show the type of logic used:

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

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

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

Show the abstract proof network:

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

Typeset a natural language argument:

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

Build a function that performs the steps of the proof:

In[8]:=
Click for copyable input
Out[8]=
In[9]:=
Click for copyable input
Out[9]=

Scope  (5)

See Also

FindEquationalProof  Reduce

Introduced in 2018
(11.3)