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_2024_proofobject, author="Wolfram Research", title="{ProofObject}", year="2019", howpublished="\url{https://reference.wolfram.com/language/ref/ProofObject.html}", note=[Accessed: 19-September-2024 ]}

BibLaTeX

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