FindEquationalProof

FindEquationalProof[thm,axms]

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

FindEquationalProof[thm,"theory"]

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:
  • expr1expr2assertion of equality
    p[expr1,…]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 expri can be arbitrary symbolic expressions, with heads representing formal operators, functions, etc.
  • The statements stmt can consist of arbitrary logical combinations of predicates.
  • FindEquationalProof[expr1&&expr2&&…,axm1&&axm2&&…] will treat each of expr1,expr2,… as a separate hypothesis, and each of axm1,axm2,… as a separate axiom.
  • FindEquationalProof[{expr1,expr2,…},{axm1,axm2,…}] is equivalent to FindEquationalProof[expr1&&expr2&&…,axm1&&axm2&&…].
  • 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 Infinityhow 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 allclose all

Basic Examples  (3)

Prove an elementary theorem in propositional logic:

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

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

Prove a theorem involving universal quantification in first-order logic:

Typeset a natural language argument:

Proof a simple syllogism:

Scope  (3)

Prove an elementary theorem from a list of axioms:

Express the theorems as a conjunction:

Show that an equational proposition cannot be derived from another:

Proof a syllogism in predicate logic using existential quantifiers:

Options  (1)

TimeConstraint  (1)

Use TimeConstraintt to limit the computation time to t seconds:

By default, FindEquationalProof looks for a proof indefinitely:

Applications  (19)

Basic Logic  (6)

Specify a choice of axioms for Boolean logic:

Prove a theorem in Boolean logic:

Show the abstract proof network:

Prove another theorem in Boolean logic:

Build and run the associated proof function:

Specify the axioms of Sheffer logic:

Prove a theorem in Sheffer logic:

Show the proof dataset:

Prove another theorem in Sheffer logic:

Build and run the associated proof function:

Prove a third theorem in Sheffer logic:

Show the abstract proof network:

Prove a final theorem in Sheffer logic:

Show the abstract proof network:

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

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

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

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

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

Prove commutativity of the logical operator Nand:

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

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

Abstract Algebra  (8)

Specify the axioms of group theory:

Prove the existence of the left identity:

Typeset a natural language argument:

Prove a more sophisticated theorem in group theory:

Show the abstract proof network:

Specify the axioms of Abelian group theory:

Prove a theorem in Abelian group theory:

Show the proof dataset:

Prove another theorem in Abelian group theory:

Show the abstract proof network:

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

Prove that every group is a semigroup:

Prove that every group is a monoid:

Define the axioms of Abelian group theory and ring theory:

Prove that every ring is an Abelian group:

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

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

Prove other relations in the group:

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

They are also left inverses because the product is commutative:

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

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

Prove that the partial order is antisymmetric:

Arithmetic  (1)

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

Prove the double-negation theorem in Presburger arithmetic:

Show the abstract proof network:

Prove a theorem regarding the addition operator in Presburger arithmetic:

Show the proof dataset:

Real Analysis  (1)

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

Prove the integration by parts formula:

Typeset a natural language argument:

Loop Theory and Universal Algebra  (1)

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

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

Show the proof dataset:

Logic Puzzles  (2)

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

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

Properties & Relations  (2)

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

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

The same is true for hypotheses:

Possible Issues  (1)

FindEquationalProof cannot prove theorems involving arithmetic operators by default:

Prove the result by specifying the properties of multiplication:

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

Text

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

CMS

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

APA

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

BibTeX

@misc{reference.wolfram_2024_findequationalproof, author="Wolfram Research", title="{FindEquationalProof}", year="2020", howpublished="\url{https://reference.wolfram.com/language/ref/FindEquationalProof.html}", note=[Accessed: 21-November-2024 ]}

BibLaTeX

@online{reference.wolfram_2024_findequationalproof, organization={Wolfram Research}, title={FindEquationalProof}, year={2020}, url={https://reference.wolfram.com/language/ref/FindEquationalProof.html}, note=[Accessed: 21-November-2024 ]}