WOLFRAM

Wolfram Language & System Documentation Center

ProofObject[…]

represents a proof object generated by FindEquationalProof.

Details
Details and Options Details and Options
Examples  
Basic Examples  
Scope  
See Also
Related Guides
History
Cite this Page

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 all close all

Basic Examples  (1)

Prove a theorem in first-order logic:

Wolfram Language code: proof = FindEquationalProof[f[f[e, e], e] == e, ForAll[a, f[a, e] == a]]

Show the theorem statement:

Wolfram Language code: proof["Theorems"]

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

Wolfram Language code: proof["ProofDataset"]

Show the abstract proof network:

Wolfram Language code: proof["ProofGraph"]

Scope  (6)

Prove a theorem in first-order logic:

Wolfram Language code: proof = FindEquationalProof[f[f[e, e], e] == e, ForAll[a, f[a, e] == a]]

Show the theorem statement:

Wolfram Language code: proof["Theorems"]

State the axioms of the theorem:

Wolfram Language code: proof["Axioms"]

Show the type of logic used:

Wolfram Language code: proof["Logic"]

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

Wolfram Language code: proof["ProofDataset"]

Show the abstract proof network:

Wolfram Language code: proof["ProofGraph"]

Typeset a natural language argument:

Wolfram Language code: proof["ProofNotebook"]

Build a function that performs the steps of the proof:

Wolfram Language code: pf = proof["ProofFunction"]
Wolfram Language code: pf[]

Specify the axioms of group theory:

Wolfram Language code: groupTheory = {ForAll[{a, b, c}, g[a, g[b, c]] == g[g[a, b], c]], ForAll[a, g[a, e] == a], ForAll[a, g[a, inv[a]] == e]}

Prove the existence of the left identity:

Wolfram Language code: proof = FindEquationalProof[ForAll[x, g[e, x] == x], groupTheory]

Show the theorem statement:

Wolfram Language code: proof["Theorems"]

State the axioms of the theorem:

Wolfram Language code: proof["Axioms"]

Show the type of logic used:

Wolfram Language code: proof["Logic"]

Specify the axioms of abelian group theory:

Wolfram Language code: abelianGroupTheory = {ForAll[{a, b, c}, g[a, g[b, c]] == g[g[a, b], c]], ForAll[a, g[a, e] == a], ForAll[a, g[a, inv[a]] == e], ForAll[{a, b}, g[a, b] == g[b, a]]}

Prove a theorem in abelian group theory:

Wolfram Language code: proof = FindEquationalProof[ForAll[{a, b, c}, g[g[g[a, b], c], inv[g[a, c]]] == b], abelianGroupTheory]

Show the proof dataset:

Wolfram Language code: ds = proof["ProofDataset"]

Extract the statement of Critical Pair Lemma 2:

Wolfram Language code: Query[Key[{"CriticalPairLemma", 2}]][ds]["Statement"]

Extract the proof of Critical Pair Lemma 2:

Wolfram Language code: Query[Key[{"CriticalPairLemma", 2}]][ds]["Proof"]

Specify some short axioms for Boolean logic:

Wolfram Language code: shortLogic = {ForAll[{a, b}, nand[nand[a, a], nand[a, b]] == a], ForAll[{a, b}, nand[a, nand[a, b]] == nand[a, nand[b, b]]], ForAll[{a, b, c}, nand[a, nand[a, nand[b, c]]] == nand[b, nand[b, nand[a, c]]]]}

Prove a theorem in Boolean algebra:

Wolfram Language code: proof = FindEquationalProof[ForAll[{a, b, c}, nand[nand[nand[a, b], c], nand[a, nand[nand[a, c], a]]] == c], shortLogic]

Show the abstract proof network:

Wolfram Language code: pg = proof["ProofGraph"]

Highlight all of the substitution lemmas:

Wolfram Language code: HighlightGraph[pg, Select[VertexList[pg], MemberQ["SubstitutionLemma"]]]

Prove a theorem in first-order logic:

Wolfram Language code: proof = FindEquationalProof[ForAll[x, f[g[x]] == g[f[x]]], ForAll[x, f[x] == g[x]]]

Typeset a natural language argument:

Wolfram Language code: proof["ProofNotebook"]

Specify the axioms of Sheffer logic:

Wolfram Language code: shefferLogic = {ForAll[a, nand[nand[a, a], nand[a, a]] == a], ForAll[{a, b}, nand[a, nand[b, nand[b, b]]] == nand[a, a]], ForAll[{a, b, c}, nand[nand[a, nand[b, c]], nand[a, nand[b, c]]] == nand[nand[nand[b, b], a], nand[nand[c, c], a]]]}

Prove a theorem in Sheffer logic:

Wolfram Language code: proof = FindEquationalProof[ForAll[{a, b}, nand[a, nand[a, b]] == nand[a, nand[b, b]]], shefferLogic]

Build (and run) the associated proof function:

Wolfram Language code: pf = proof["ProofFunction"]
Wolfram Language code: pf[]
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_2026_proofobject, author="Wolfram Research", title="{ProofObject}", year="2019", howpublished="\url{https://reference.wolfram.com/language/ref/ProofObject.html}", note=[Accessed: 13-June-2026]}

BibLaTeX

@online{reference.wolfram_2026_proofobject, organization={Wolfram Research}, title={ProofObject}, year={2019}, url={https://reference.wolfram.com/language/ref/ProofObject.html}, note=[Accessed: 13-June-2026]}