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
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. |
"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 |
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]= | ![]() |
This work is licensed under a Creative Commons Attribution 4.0 International License