Wolfram Research

Function Repository Resource:

FindEquationalPath (1.0.0) current version: 1.0.1 »

Source Notebook

Find a path that goes from one expression to another with a sequence of replacements

Contributed by: Nikolay Murzin

ResourceFunction["FindEquationalPath"][theorem, axioms]

finds a replacement path from the left-hand side of a theorem to its right-hand side using replacements specified by axioms.

ResourceFunction["FindEquationalPath"][proof]

find a path for the precomputed ProofObject proof.

ResourceFunction["FindEquationalPath"][, hypothesis]

specify an explicit hypothesis lemma from the underlying ProofObject to return a path for.

ResourceFunction["FindEquationalPath"][,hypothesis,conclusion]

specify an explicit conclusion lemma from the underlying ProofObject to be used in path construction.

ResourceFunction["FindEquationalPath"][,prop]

returns a specified property prop of a replacement path.

Details and Options

ResourceFunction["FindEquationalPath"] uses FindEquationalProof to find a proof of equational proposition and by using cut-elimination, derives a sequential path of one-step replacements from one side of a theorem to another.
The replacement path consists of pattern expressions corresponding to logic formulas with patterns (like a Blank, a_) representing universal variables (ForAll) and other symbols representing functional constants (Exists).
Properties prop supported by ResourceFunction["FindEquationalPath"] include:
"ProofObject"the corresponding ProofObject
"Path"a list of expressions comprising a found path (default)
"Justification"a list of axioms used in each subsequent step of a path together with its orientation and position
"Rewrites"a list of rewriting functions that reproduce a path
"RewritesTest"test rewriting functions to successfully reproduce a path
Allall of the above as an association
For the "Justification" property, axiom orientation is a direction of a corresponding rule, for example a==b can be used as a b (right orientation) or b a (left orientation).
Position of a step is a position of a subexpression at which a rule corresponding to an axiom is being applied.
Explicit hypothesis and conclusion lemmas are keys from the "Proof" or "ProofDataset" properties of a ProofObject, with {"Hypothesis", 1} and corresponding {"Conclusion", 1} being the default.
Explicit conclusion lemma is rarely needed, it is used as a starting point to generate a path by backtracking through a proof graph.
ResourceFunction["FindEquationalPath"] takes the option "Reverse". With "Reverse"True, a reversed replacement path is returned.

Examples

Basic Examples (3) 

Find a replacement path given a set of equations:

In[1]:=
ResourceFunction["FindEquationalPath"][a == d, a == b && b == c && c == d]
Out[1]=

Find a replacement path using universally quantified equations:

In[2]:=
ResourceFunction["FindEquationalPath"][
 ForAll[{x, y}, plus[x, plus[y, 0]] == plus[x, plus[0, y]]], {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]]]}]
Out[2]=

Find a much more complicated path:

In[3]:=
ResourceFunction["FindEquationalPath"][
  ForAll[{a, b}, or[not[or[not[a], b]], not[or[not[a], not[b]]]] == a], {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]]]}] // Short
Out[3]=

Scope (7) 

Use names from the AxiomaticTheory for a list of axioms and its notable theorems:

In[4]:=
ResourceFunction["FindEquationalPath", ResourceVersion->"1.0.0"]["AbsorptionOrAnd", "BooleanAxioms"]
Out[4]=

Specify a custom theorem with AxiomaticTheory axioms:

In[5]:=
ResourceFunction["FindEquationalPath", ResourceVersion->"1.0.0"][((a\[CircleTimes]b)\[CircleTimes]c)\[CircleTimes]
\!\(\*OverscriptBox[\(a\[CircleTimes]c\), \(_\)]\) == b, "AbelianGroupAxioms"]
Out[5]=

Use a ProofObject to find a replacement path:

In[6]:=
proof = FindEquationalProof["DoubleNegation", "BooleanAxioms"]
Out[6]=
In[7]:=
ResourceFunction["FindEquationalPath"][proof]
Out[7]=

Specify a lemma or a different hypothesis from a proof to construct a path for:

In[8]:=
ResourceFunction["FindEquationalPath"][
 FindEquationalProof["DoubleNegation", "BooleanAxioms"], {"CriticalPairLemma", 5}]
Out[8]=
In[9]:=
ResourceFunction["FindEquationalPath"]["DeMorgan", "BooleanAxioms", {"Hypothesis", 2}] // Short
Out[9]=

Find a replacement path in a string substitution system:

In[10]:=
proof = ResourceFunction["FindStringProof"][
  "AAA" <-> "BBABAA", {"AA" <-> "BAA", "BAA" <-> "AB"}]
Out[10]=
In[11]:=
ResourceFunction["FindEquationalPath"][
   proof] /. {c : A | B :> ToString[c], CircleDot -> StringJoin} // DeleteAdjacentDuplicates
Out[11]=

Find a replacement path in a Wolfram model system:

In[12]:=
proof = ResourceFunction[
   "FindWolframModelProof"][{{1, 2}} <-> {{1, 2}, {1, 3}, {4, 1}, {5, 4}}, {{x, y}} <-> {{x, y}, {y, z}}]
Out[12]=
In[13]:=
ResourceFunction["WolframModelPlot"][#, VertexLabels -> Automatic] & /@
  Reverse[
  First /@ Gather[Sort /@ (List /@ ResourceFunction["FindEquationalPath"][
         proof] /. {CircleMinus | CirclePlus | CircleTimes -> List, CircleDot -> Sequence})]
  ]
Out[13]=

Reproduce the replacement path using rewriting functions:

In[14]:=
rewrites = ResourceFunction["FindEquationalPath"]["Absorption", "BooleanAxioms", "Rewrites"];
In[15]:=
FoldList[#2[#1] &, \[FormalA]_\[CircleTimes](\[FormalA]_\[CirclePlus]\[FormalB]_), rewrites]
Out[15]=

Options (1) 

Reverse (1) 

Reverse a path:

In[16]:=
ResourceFunction["FindEquationalPath"][a == d, a == b && b == c && c == d, "Reverse" -> True]
Out[16]=

Neat Examples (3) 

Find a replacement path for a well known syllogism by specifying an existentially quantified goal:

In[17]:=
ResourceFunction["FindEquationalPath"][\!\(
\*SubscriptBox[\(\[Exists]\), \(x\)]\(Mortal[x]\)\), {\!\(
\*SubscriptBox[\(\[ForAll]\), \(x\)]\((Man[x] \[Implies] Mortal[x])\)\), \!\(
\*SubscriptBox[\(\[Exists]\), \(x\)]\(Man[x]\)\)}, "Reverse" -> True] /. {p_ \!\(\*
TagBox["||",
"InactiveToken",
BaseStyle->"Inactive",
SyntaxForm->"||"]\) \!\(\*
TagBox["!",
"InactiveToken",
BaseStyle->"Inactive",
SyntaxForm->"!"]\) p_ :> True, \!\(\*
TagBox["!",
"InactiveToken",
BaseStyle->"Inactive",
SyntaxForm->"!"]\) p_ \!\(\*
TagBox["||",
"InactiveToken",
BaseStyle->"Inactive",
SyntaxForm->"||"]\) q_ :> p \!\(\*
TagBox["\[Implies]",
"InactiveToken",
BaseStyle->"Inactive",
SyntaxForm->"\[Implies]"]\) q} // Column
Out[17]=

Test Boolean theorems:

In[18]:=
AssociationMap[
  ResourceFunction["FindEquationalPath"][#, "BooleanAxioms", All][
      "RewriteTest"] & /@ AxiomaticTheory["BooleanAxioms", "NotableTheorems"][#] &, Keys@AxiomaticTheory["BooleanAxioms", "NotableTheorems"]] // Short
Out[18]=

An example from A New Kind of Science (p. 775):

In[19]:=
proof = FindEquationalProof[p\[CenterDot]q == q\[CenterDot]p, {\!\(
\*SubscriptBox[\(\[ForAll]\), \(\[FormalA]\)]\(\((\[FormalA]\[CenterDot]\[FormalA])\)\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalA])\)\)\) \[Implies] \[FormalA], \!\(
\*SubscriptBox[\(\[ForAll]\), \({\[FormalA], \[FormalB]}\)]\(\[FormalA] == \((\[FormalA]\[CenterDot]\[FormalA])\)\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalB])\)\)\), \!\(
\*SubscriptBox[\(\[ForAll]\), \({\[FormalA], \[FormalB]}\)]\(\[FormalA]\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalB])\) == \[FormalA]\[CenterDot]\((\[FormalB]\[CenterDot]\[FormalB])\)\)\), \!\(
\*SubscriptBox[\(\[ForAll]\), \({\[FormalA], \[FormalB], \[FormalC]}\)]\(\((\[FormalA]\[CenterDot]\((\[FormalA]\[CenterDot]\((\[FormalB]\[CenterDot]\[FormalC])\))\))\) == \((\[FormalB]\[CenterDot]\((\[FormalB]\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalC])\))\))\)\)\)}]
Out[19]=
In[20]:=
path = ResourceFunction["FindEquationalPath"][proof]
Out[20]=

It is two steps shorter, but it uses a reverse of one axiom:

In[21]:=
Column[Style[#, 8] & /@ ResourceFunction["FindEquationalPath"][proof, "Path"], Frame -> All]
Out[21]=

Prove the existential version of the same theorem using a proof by refutation:

In[22]:=
ResourceFunction["FindEquationalPath"][
 Exists[{p, q}, p\[CenterDot]q == q\[CenterDot]p], {\!\(
\*SubscriptBox[\(\[ForAll]\), \(\[FormalA]\)]\(\((\[FormalA]\[CenterDot]\[FormalA])\)\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalA])\)\)\) \[Implies] \[FormalA], \!\(
\*SubscriptBox[\(\[ForAll]\), \({\[FormalA], \[FormalB]}\)]\(\[FormalA] == \((\[FormalA]\[CenterDot]\[FormalA])\)\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalB])\)\)\), \!\(
\*SubscriptBox[\(\[ForAll]\), \({\[FormalA], \[FormalB]}\)]\(\[FormalA]\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalB])\) == \[FormalA]\[CenterDot]\((\[FormalB]\[CenterDot]\[FormalB])\)\)\), \!\(
\*SubscriptBox[\(\[ForAll]\), \({\[FormalA], \[FormalB], \[FormalC]}\)]\(\((\[FormalA]\[CenterDot]\((\[FormalA]\[CenterDot]\((\[FormalB]\[CenterDot]\[FormalC])\))\))\) == \((\[FormalB]\[CenterDot]\((\[FormalB]\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalC])\))\))\)\)\)}]
Out[22]=

Version History

  • 1.0.1 – 25 January 2023
  • 1.0.0 – 20 January 2023

Related Resources

License Information