Wolfram Language & System Documentation Center

FindEquationalProof

tries to find an equational proof of the symbolic theorem thm using the axioms axms.

tries to find a proof of thm using the specified named axiomatic theory.

Details and Options

If FindEquationalProof[thm,axms] succeeds in deriving the theorem thm from the axioms axms, then it returns a ProofObject expression. If it succeeds in showing that the theorem cannot be derived from the axioms, it returns a Failure object. Otherwise, it may not terminate unless time constrained.
Axioms and theorems can be given in equational form or as formulas in first-order logic. Formulas in first-order logic are converted to an equational form.
The statements thm and axms can be any logical combination of terms of the form:

	expr₁expr₂	assertion of equality
	p[expr₁,…]	arbitrary symbolic predicate
	ForAll[vars,stmt]	assertion that stmt is true for all values of vars
	Exists[vars,stmt]	assertion that values of vars exist for which stmt is true

The expr_i can be arbitrary symbolic expressions, with heads representing formal operators, functions, etc.
The statements stmt can consist of arbitrary logical combinations of predicates.
FindEquationalProof[expr₁&&expr₂&&…,axm₁&&axm₂&&…] will treat each of expr₁,expr₂,… as a separate hypothesis, and each of axm₁,axm₂,… as a separate axiom.
FindEquationalProof[{expr₁,expr₂,…},{axm₁,axm₂,…}] is equivalent to FindEquationalProof[expr₁&&expr₂&&…,axm₁&&axm₂&&…].
FindEquationalProof[thm,"theory"] is equivalent to FindEquationalProof[thm,AxiomaticTheory["theory"]].
FindEquationalProof["name","theory"] tries to find a proof of the named theorem from AxiomaticTheory["theory","NotableTheorems"].
FindEquationalProof has the following option:
TimeConstraint Infinity how much time to allow
If FindEquationalProof exceeds the specified time constraint, it returns a Failure object.
FindEquationalProof[thm,axms] uses the Knuth–Bendix completion algorithm to prove that the theorem thm follows from the axioms axms.

Examples

open all close all

Basic Examples (3)

Prove an elementary theorem in propositional logic:

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

Show the abstract proof network, with tooltips showing the intermediate expressions:

Wolfram Language code: proof["ProofGraph"]

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

Wolfram Language code: proof["ProofDataset"]

Prove a theorem involving universal quantification 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"]

Proof a simple syllogism:

Wolfram Language code: FindEquationalProof[mortal[socrates], {ForAll[x, Implies[man[x], mortal[x]]], man[socrates]}]

Scope (3)

Prove an elementary theorem from a list of axioms:

Wolfram Language code: FindEquationalProof[a == d, {a == b, b == c, c == d}]

Express the theorems as a conjunction:

Wolfram Language code: FindEquationalProof[a == d, a == b && b == c && c == d]

Show that an equational proposition cannot be derived from another:

Wolfram Language code: FindEquationalProof[a == c, a == b]

Proof a syllogism in predicate logic using existential quantifiers:

Wolfram Language code: FindEquationalProof[Exists[x, Mortal[x]], {ForAll[x, Implies[Man[x], Mortal[x]]], Exists[x, Man[x]]}]

Options (1)

TimeConstraint (1)

Use TimeConstraintt to limit the computation time to t seconds:

Wolfram Language code: theorem = ForAll[{a, b, c}, f[a, f[a, f[b, c]]] == f[b, f[b, f[a, c]]]]

Wolfram Language code:

axiom = ForAll[{a, b, c}, f[f[a, a], f[a, a]] == a && f[a, f[b, f[b, b]]] == f[a, a] && f[f[a, f[b, c]], f[a, f[b, c]]] == f[f[f[b, b], a], f[f[c, c], a]]]

Wolfram Language code: FindEquationalProof[theorem, axiom, TimeConstraint -> 1]

By default, FindEquationalProof looks for a proof indefinitely:

Wolfram Language code: FindEquationalProof[theorem, axiom]//AbsoluteTiming

Applications (19)

Basic Logic (6)

Specify a choice of axioms for Boolean logic:

Wolfram Language code:

booleanLogic = {ForAll[{a, b}, and[a, b] == and[b, a]], ForAll[{a, b}, or[a, b] == or[b, a]], ForAll[{a, b}, and[a, or[b, not[b]]] == a], ForAll[{a, b}, or[a, and[b, not[b]]] == a], ForAll[{a, b, c}, and[a, or[b, c]] == or[and[a, b], and[a, c]]], ForAll[{a, b, c}, or[a, and[b, c]] == and[or[a, b], or[a, c]]]}

Prove a theorem in Boolean logic:

Wolfram Language code: proof = FindEquationalProof[ForAll[{a, b}, or[not[or[not[a], b]], not[or[not[a], not[b]]]] == a], booleanLogic]

Show the abstract proof network:

Wolfram Language code: proof["ProofGraph"]

Prove another theorem in Boolean logic:

Wolfram Language code: proof2 = FindEquationalProof[ForAll[{a, b}, not[or[not[or[a, b]], not[or[a, not[b]]]]] == a], booleanLogic]

Build and run the associated proof function:

Wolfram Language code: proof2["ProofFunction"][]

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]

Show the proof dataset:

Wolfram Language code: proof["ProofDataset"]

Prove another theorem in Sheffer logic:

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

Build and run the associated proof function:

Wolfram Language code: proof2["ProofFunction"][]

Prove a third theorem in Sheffer logic:

Wolfram Language code:

proof3 = FindEquationalProof[ForAll[{a, b, c}, nand[nand[nand[a, b], c], nand[a, nand[nand[a, c], a]]] == c], shefferLogic]

Show the abstract proof network:

Wolfram Language code: proof3["ProofGraph"]

Prove a final theorem in Sheffer logic:

Wolfram Language code:

proof4 = FindEquationalProof[ForAll[{a, b, c}, nand[a, nand[a, nand[b, c]]] == nand[b, nand[b, nand[a, c]]]], shefferLogic]

Show the abstract proof network:

Wolfram Language code: proof4["ProofGraph"]

Define the axioms of Boolean logic, Huntington logic and Robbins logic:

Wolfram Language code:

booleanLogic = {ForAll[{a, b}, and[a, b] == and[b, a]], ForAll[{a, b}, or[a, b] == or[b, a]], ForAll[{a, b}, and[a, or[b, not[b]]] == a], ForAll[{a, b}, or[a, and[b, not[b]]] == a], ForAll[{a, b, c}, and[a, or[b, c]] == or[and[a, b], and[a, c]]], ForAll[{a, b, c}, or[a, and[b, c]] == and[or[a, b], or[a, c]]]}

Wolfram Language code:

huntingtonLogic = {ForAll[{a, b}, or[a, b] == or[b, a]], ForAll[{a, b, c}, or[a, or[b, c]] == or[or[a, b], c]], ForAll[{a, b}, or[not[or[not[a], b]], not[or[not[a], not[b]]]] == a]}

Wolfram Language code:

robbinsLogic = {ForAll[{a, b}, or[a, b] == or[b, a]], ForAll[{a, b, c}, or[a, or[b, c]] == or[or[a, b], c]], ForAll[{a, b}, not[or[not[or[a, b]], not[or[a, not[b]]]]] == a]}

Prove that the axioms of Huntington logic follow from the axioms of Boolean logic:

Wolfram Language code: FindEquationalProof[huntingtonLogic, booleanLogic]

Prove that the axioms of Robbins logic follow from the axioms of Boolean logic:

Wolfram Language code: FindEquationalProof[robbinsLogic, booleanLogic]

Prove that the axioms of Robbins logic follow from the axioms of Huntington logic:

Wolfram Language code: FindEquationalProof[robbinsLogic, huntingtonLogic]

Define Wolfram's shortest-possible axiom for Boolean algebra:

Wolfram Language code: wolframLogic = ForAll[{a, b, c}, ((a·b)·c)·(a·((a·c)·a)) == c]

Prove commutativity of the logical operator Nand:

Wolfram Language code: FindEquationalProof[a·b == b·a, wolframLogic]

Wolfram Language code: %["ProofGraph"]

Use the Wolfram axiom to prove the Boolean axioms by introducing the And, Or, Not operators via ancillary definitions:

Wolfram Language code: ancillary = AxiomaticTheory["WolframAxioms", "AncillaryDefinitions"]

Wolfram Language code: FindEquationalProof[AxiomaticTheory["BooleanAxioms"], Join[AxiomaticTheory["WolframAxioms"], Values[ancillary]]]

Use the Wolfram axiom to prove the Or-Not Boolean axiom by introducing the Or, Not operators via ancillary definitions:

Wolfram Language code: theorem = AxiomaticTheory["OrNotBooleanAxioms"]

Wolfram Language code: ancillary = AxiomaticTheory["WolframAxioms", "AncillaryDefinitions"]

Wolfram Language code: FindEquationalProof[theorem, Join[AxiomaticTheory["WolframAxioms"], Values[ancillary]]]

Abstract Algebra (8)

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]

Typeset a natural language argument:

Wolfram Language code: proof["ProofNotebook"]

Prove a more sophisticated theorem in group theory:

Wolfram Language code:

proof2 = FindEquationalProof[ForAll[{a, b, c, d}, g[a, inv[g[b, g[g[g[c, inv[c]], inv[g[d, b]]], a]]]] == d], groupTheory]

Show the abstract proof network:

Wolfram Language code: proof2["ProofGraph"]

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: proof["ProofDataset"]

Prove another theorem in Abelian group theory:

Wolfram Language code:

proof2 = FindEquationalProof[ForAll[{a, b, c, d}, g[a, inv[g[b, g[g[g[c, inv[c]], inv[g[d, b]]], a]]]] == d], abelianGroupTheory]

Show the abstract proof network:

Wolfram Language code: proof2["ProofGraph"]

Define the axioms of semigroup theory, monoid theory and group theory:

Wolfram Language code: semigroupTheory = ForAll[{a, b, c}, g[a, g[b, c]] == g[g[a, b], c]]

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

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 that every group is a semigroup:

Wolfram Language code: FindEquationalProof[semigroupTheory, groupTheory]

Prove that every group is a monoid:

Wolfram Language code: FindEquationalProof[monoidTheory, groupTheory]

Define the axioms of Abelian group theory and ring 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]]}

Wolfram Language code:

ringTheory = {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]], ForAll[{a, b, c}, f[a, f[b, c]] == f[f[a, b], c]], ForAll[{a, b, c}, f[a, g[b, c]] == g[f[a, b], f[a, c]]], ForAll[{a, b}, f[a, b] == f[b, a]]}

Prove that every ring is an Abelian group:

Wolfram Language code: FindEquationalProof[abelianGroupTheory, ringTheory]["ProofGraph"]

Take the axioms of group theory, using p as product and e as identity element:

Wolfram Language code: groups = AxiomaticTheory[{"GroupAxioms", "Multiplication" -> p, "Identity" -> e}]

Add the relations generating the quaternion group from two of its eight elements:

Wolfram Language code: quaternionGroup = {groups, p[p[a, b], a] == b, p[p[b, a], b] == a};

Prove other relations in the group:

Wolfram Language code: FindEquationalProof[p[a, a] == p[b, b], quaternionGroup]

Wolfram Language code: FindEquationalProof[p[p[p[a, a], a], a] == e, quaternionGroup]

Wolfram Language code: FindEquationalProof[p[p[p[b, b], b], b] == e, quaternionGroup]

The axioms of field theory include the existence of multiplicative right inverses:

Wolfram Language code: AxiomaticTheory["FieldAxioms", "AxiomsAssociation"]["MultiplicationInverse"]

They are also left inverses because the product is commutative:

Wolfram Language code:

FindEquationalProof[ForAll[, Implies[Not[Tilde[, OverTilde[0]]], Tilde[CircleTimes[SuperMinus[], ], OverTilde[1]]]], "FieldAxioms"]

Show the axioms of right-near rings from those of left-near rings by specifying that the product is commutative:

Wolfram Language code:

FindEquationalProof[AxiomaticTheory["RightNearRingAxioms"], Join[AxiomaticTheory["LeftNearRingAxioms"], {ForAll[{, }, CircleTimes[, ] == CircleTimes[, ]]}]]

Construct the axioms of an idempotent semiring with a naturally defined partial order denoted by LeftTriangle:

Wolfram Language code:

axioms = Join[AxiomaticTheory["SemiringAxioms"] /. Equal -> Tilde, {Subscript[∀, ]∼, Subscript[∀, {, }](∼∼), Subscript[∀, {, , }](∼ && ∼∼), ForAll[, Tilde[CirclePlus[, ], ]], ForAll[{, }, Implies[LeftTriangle[, ], Tilde[CirclePlus[, ], ]]], ForAll[{, }, Implies[Tilde[CirclePlus[, ], ], LeftTriangle[, ]]]}]

Prove that the partial order is antisymmetric:

Wolfram Language code: theorem = ForAll[{, }, Implies[And[LeftTriangle[, ], LeftTriangle[, ]], Tilde[, ]]]

Wolfram Language code: FindEquationalProof[theorem, axioms]

Arithmetic (1)

Specify some axioms for a modified (equational) version of Presburger arithmetic:

Wolfram Language code:

presburgerArithmetic = {ForAll[x, plus[x, 0] == x], ForAll[x, plus[x, neg[x]] == 0], ForAll[{x, y, z}, plus[plus[x, y], z] == plus[x, plus[y, z]]]}

Prove the double-negation theorem in Presburger arithmetic:

Wolfram Language code: proof = FindEquationalProof[ForAll[x, neg[neg[x]] == x], presburgerArithmetic]

Show the abstract proof network:

Wolfram Language code: proof["ProofGraph"]

Prove a theorem regarding the addition operator in Presburger arithmetic:

Wolfram Language code: proof2 = FindEquationalProof[ForAll[{x, y}, plus[x, plus[y, 0]] == plus[x, plus[0, y]]], presburgerArithmetic]

Show the proof dataset:

Wolfram Language code: proof2["ProofDataset"]

Real Analysis (1)

These axioms specify the fundamental theorem of calculus, the product rule and the linearity of differentiation:

Wolfram Language code:

calculus = {ForAll[f, integral[derivative[f]] == f], ForAll[f, derivative[integral[f]] == f], ForAll[{f, g}, derivative[product[f, g]] == sum[product[f, derivative[g]], product[g, derivative[f]]]], ForAll[{f, g}, derivative[sum[f, g]] == sum[derivative[f], derivative[g]]]}

Prove the integration by parts formula:

Wolfram Language code:

proof = FindEquationalProof[ForAll[{f, g}, sum[integral[product[f, derivative[g]]], integral[product[g, derivative[f]]]] == product[f, g]], calculus]

Typeset a natural language argument:

Wolfram Language code: proof["ProofNotebook"]

Loop Theory and Universal Algebra (1)

These axioms describe a loop whose group of inner automorphisms is Abelian:

Wolfram Language code:

loopTheory = {ForAll[x, mult[x, 1] == x], ForAll[x, mult[1, x] == x], ForAll[{x, y}, mult[x, conj[x, y]] == y], ForAll[{x, y, z}, R[x, y, z] == z], ForAll[{x, y, z, u}, T[x, R[y, z, u]] == R[y, z, T[x, y]]], ForAll[{x, y}, T[x, y] == conj[x, mult[y, x]]]}

Prove that the nilpotency class of this loop is less than or equal to 3:

Wolfram Language code:

proof = FindEquationalProof[ForAll[{x, y, z, u, v}, mult[comm[x, assc[y, z, u]], v] == mult[v, comm[x, assc[y, z, u]]]], loopTheory]

Show the proof dataset:

Wolfram Language code: proof["ProofDataset"]

Logic Puzzles (2)

Conclude, following Lewis Carroll, that babies cannot manage crocodiles:

Wolfram Language code:

FindEquationalProof[Not[Exists[x, And[baby[x], manageCrocodile[x]]]], {ForAll[x, Implies[baby[x], Not[logical[x]]]], ForAll[x, Implies[manageCrocodile[x], Not[despised[x]]]], ForAll[x, Implies[Not[logical[x]], despised[x]]]}]

Check the solution of a knights (who always tell the truth) and knaves (who always lie) puzzle:

Wolfram Language code:

FindEquationalProof[And[knight[zoey], knave[mel]], {ForAll[p, ForAll[s, Implies[And[knight[p], says[p, s]], s]]], ForAll[p, ForAll[s, Implies[And[knave[p], says[p, s]], Not[s]]]], ForAll[p, Or[knight[p], knave[p]]], says[zoey, knave[mel]], says[mel, And[Not[knave[zoey]], Not[knave[mel]]]]}]

Properties & Relations (2)

If FindEquationalProof returns a proof object for a particular theorem, then FullSimplify will return True for that theorem:

Wolfram Language code: FindEquationalProof[f[f[u, f[v, w]], u] == f[u, f[f[v, w], u]], ForAll[{a, b, c}, f[a, f[b, c]] == f[f[a, b], c]]]

Wolfram Language code: FullSimplify[f[f[u, f[v, w]], u] == f[u, f[f[v, w], u]], ForAll[{a, b, c}, f[a, f[b, c]] == f[f[a, b], c]]]

FindEquationalProof treats lists of axioms and conjunctions of axioms as equivalent:

Wolfram Language code: FindEquationalProof[a == c, {a == b, b == c}]

Wolfram Language code: FindEquationalProof[a == c, a == b && b == c]

The same is true for hypotheses:

Wolfram Language code: FindEquationalProof[{a == c, a == d}, {a == b, b == c, c == d}]

Wolfram Language code: FindEquationalProof[a == c && a == d, a == b && b == c && c == d]

Possible Issues (1)

FindEquationalProof cannot prove theorems involving arithmetic operators by default:

Wolfram Language code: FindEquationalProof[ForAll[x, f[4 * x] == 4 * f[x]], {ForAll[x, f[2 * x] == 2 * f[x]]}]

Prove the result by specifying the properties of multiplication:

Wolfram Language code:

FindEquationalProof[ForAll[a, f[mult[4, x]] == mult[4, f[x]]], {ForAll[x, f[mult[2, x]] == mult[2, f[x]]], ForAll[{x, y, z}, mult[x, mult[y, z]] == mult[mult[x, y], z]], mult[2, 2] == 4}]

Top

More Learning

Tech Support

Wolfram Solutions

Wolfram Solutions For Education

Get Started

Grow Your Skills

Work with Us

Educational Programs for Adults

Educational Programs for Youth

Read

FindEquationalProof

Details and Options

Examples

Basic Examples (3)

Scope (3)

Options (1)

TimeConstraint (1)

Applications (19)

Basic Logic (6)

Abstract Algebra (8)

Arithmetic (1)

Real Analysis (1)

Loop Theory and Universal Algebra (1)

Logic Puzzles (2)

Properties & Relations (2)

Possible Issues (1)

Text

CMS

APA

BibTeX

BibLaTeX

FindEquationalProof

Details and Options

Examples

Basic Examples (3)

Scope (3)

Options (1)

TimeConstraint (1)

Applications (19)

Basic Logic (6)

Abstract Algebra (8)

Arithmetic (1)

Real Analysis (1)

Loop Theory and Universal Algebra (1)

Logic Puzzles (2)

Properties & Relations (2)

Possible Issues (1)

See Also

Related Guides

Related Links

History

Text

CMS

APA

BibTeX

BibLaTeX