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:

Wolfram Research (2018), ProofObject, Wolfram Language function, https://reference.wolfram.com/language/ref/ProofObject.html (updated 2019).

Text

Wolfram Research (2018), ProofObject, Wolfram Language function, https://reference.wolfram.com/language/ref/ProofObject.html (updated 2019).

CMS

Wolfram Language. 2018. "ProofObject." Wolfram Language & System Documentation Center. Wolfram Research. Last Modified 2019. https://reference.wolfram.com/language/ref/ProofObject.html.

APA

Wolfram Language. (2018). ProofObject. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/ProofObject.html

BibTeX

@misc{reference.wolfram_2023_proofobject, author="Wolfram Research", title="{ProofObject}", year="2019", howpublished="\url{https://reference.wolfram.com/language/ref/ProofObject.html}", note=[Accessed: 18-April-2024 ]}

BibLaTeX

@online{reference.wolfram_2023_proofobject, organization={Wolfram Research}, title={ProofObject}, year={2019}, url={https://reference.wolfram.com/language/ref/ProofObject.html}, note=[Accessed: 18-April-2024 ]}