# 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:
•  expr1expr2 assertion 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 Infinity how much time to allow
• If FindEquationalProof exceeds the specified time constraint, it returns a Failure object.
• FindEquationalProof[thm,axms] uses the KnuthBendix 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 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: