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
    "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:

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:

Introduced in 2018
 (11.3)
 |
Updated in 2019
 (12.0)