# Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

Function Repository Resource:

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

Contributed by:
Nikolay Murzin

ResourceFunction["FindEquationalPath"][ finds a replacement path from the left-hand side of a | |

ResourceFunction["FindEquationalPath"][ find a path for the precomputed ProofObject | |

ResourceFunction["FindEquationalPath"][…, specify an explicit | |

ResourceFunction["FindEquationalPath"][…, specify an explicit | |

ResourceFunction["FindEquationalPath"][…, returns a specified property |

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 |

All | all 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.

Find a replacement path given a set of equations:

In[1]:= |

Out[1]= |

Find a replacement path using universally quantified equations:

In[2]:= |

Out[2]= |

Find a much more complicated path:

In[3]:= |

Out[3]= |

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

In[4]:= |

Out[4]= |

Specify a custom theorem with AxiomaticTheory axioms:

In[5]:= |

Out[5]= |

Use a ProofObject to find a replacement path:

In[6]:= |

Out[6]= |

In[7]:= |

Out[7]= |

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

In[8]:= |

Out[8]= |

In[9]:= |

Out[9]= |

Find a replacement path in a string substitution system:

In[10]:= |

Out[10]= |

In[11]:= |

Out[11]= |

Find a replacement path in a Wolfram model system:

In[12]:= |

Out[12]= |

In[13]:= |

Out[13]= |

Reproduce the replacement path using rewriting functions:

In[14]:= |

In[15]:= |

Out[15]= |

Reverse a path:

In[16]:= |

Out[16]= |

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

In[17]:= |

Out[17]= |

Test Boolean theorems:

In[18]:= |

Out[18]= |

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

In[19]:= |

Out[19]= |

In[20]:= |

Out[20]= |

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

In[21]:= |

Out[21]= |

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

In[22]:= |

Out[22]= |

- 1.0.1 – 25 January 2023
- 1.0.0 – 20 January 2023

This work is licensed under a Creative Commons Attribution 4.0 International License