Warning: This resource is provisional

Function Repository Resource:

# FindReplacePath

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

Contributed by: Nikolay Murzin
 ResourceFunction["FindReplacePath"][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["FindReplacePath"][theorem,axioms,prop] return a specified property of a path.

## Details and Options

ResourceFunction["FindReplacePath"] uses FindEquationalProof to find a proof of an equational proposition, and by process of cut-elimination it derives a sequential path of one-step replacements from one side of a theorem to the other.
The path consists of pattern expressions corresponding to logic formulas with patterns (like a_) representing universal variables (ForAll) and other symbols representing functional constants (Exists).
The list of ResourceFunction["FindReplacePath"] properties includes:
 "ProofObject" corresponding ProofObject "Path" list of expressions constituting a found path (default) "Justification" list of axioms used in each subsequent step of a path together with their orientations and positions "Rewrites" list of rewriting functions that reproduce a path "PathTest" test path endpoints to match a required statement "RewritesTest" test-rewriting functions to successfully reproduce a path All all of the above as an association

## Examples

### Basic Examples (2)

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]=
 In[3]:=
 Out[3]=
 In[4]:=
 Out[4]=
 In[5]:=
 Out[5]=
 In[6]:=
 Out[6]=

### Scope (5)

Use names from AxiomaticTheory:

 In[7]:=
 Out[7]=

Use ProofObject to find a path:

 In[8]:=
 Out[8]=
 In[9]:=
 Out[9]=

Find a path in a string substitution system:

 In[10]:=
 Out[10]=
 In[11]:=
 Out[11]=

Find a path in a Wolfram model system:

 In[12]:=
 Out[12]=
 In[13]:=
 Out[13]=

Reproduce the found path using rewriting functions:

 In[14]:=
 Out[14]=
 In[15]:=
 Out[15]=

### Possible Issues (1)

Degenerate axiom systems capable of deriving a==b-type statements can sometimes fail:

 In[16]:=
 Out[16]=
 In[17]:=
 Out[17]=

### Neat Examples (2)

Test Boolean theorems:

 In[18]:=
 Out[18]=

NKS example:

 In[19]:=
 Out[19]=
 In[20]:=
 Out[20]=

This result is two steps shorter than the NKS path, but it uses the reverse of one axiom:

 In[21]:=
 Out[21]=

## Version History

• 1.0.0 – 07 February 2022