# 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 "ProofGraphWeighted" abstract proof network with central lemmas emphasized "ProofLength" number of steps in the proof "ProofNotebook" proof written out in a notebook "ProofFunction" function for validating rewrite rules "Theorems" statement of theorems "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:

Show the theorem statement:

State the axioms of the theorem:

Show the type of logic used:

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

Show the abstract proof network:

Typeset a natural language argument:

Build a function that performs the steps of the proof:

## Scope(5)

Specify the axioms of group theory:

Prove the existence of the left identity:

Show the theorem statement:

State the axioms of the theorem:

Show the type of logic used:

Specify the axioms of abelian group theory:

Prove a theorem in abelian group theory:

Show the proof dataset:

Extract the statement of Critical Pair Lemma 2:

Extract the proof of Critical Pair Lemma 2:

Specify some short axioms for Boolean logic:

Prove a theorem in Boolean algebra:

Show the abstract proof network:

Highlight all of the substitution lemmas:

Prove a theorem in first-order logic:

Typeset a natural language argument:

Specify the axioms of Sheffer logic:

Prove a theorem in Sheffer logic:

Build (and run) the associated proof function: