Wolfram Research

Function Repository Resource:

FindListProof

Source Notebook

Try to find a proof of equivalence between lists in a given multiway system

Contributed by: Jonathan Gorard

ResourceFunction["FindListProof"][thm,axms]

tries to find a proof of the list equivalence theorem thm using the multiway system axioms axms.

Details and Options

If ResourceFunction["FindListProof"][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.
ResourceFunction["FindListProof"] accepts both individual axioms and lists of axioms, and likewise for theorems.
ResourceFunction["FindListProof"] has the following option:
TimeConstraint Infinity how much time to allow
If ResourceFunction["FindListProof"] exceeds the specified time constraint, it returns a Failure object.
ResourceFunction["FindListProof"][thm,axms] uses the KnuthBendix completion algorithm to prove that the theorem thm follows from the axioms axms.

Examples

Basic Examples (2) 

Prove an elementary theorem regarding the equivalence of two lists in a simple multiway system:

In[1]:=
proof = ResourceFunction[
  "FindListProof"][{0, 0} <-> {0, 1, 0, 1}, {0} <-> {0, 1}]
Out[1]=

Show the abstract proof network, with tooltips showing the intermediate expressions:

In[2]:=
proof["ProofGraph"]
Out[2]=

Show the complete list of proof steps as a Dataset object:

In[3]:=
proof["ProofDataset"]
Out[3]=

Typeset a natural language argument:

In[4]:=
proof["ProofNotebook"]
Out[4]=

Prove a more sophisticated theorem involving multiple rules and hypotheses:

In[5]:=
proof = ResourceFunction[
  "FindListProof"][{{0, 0, 0} <-> {1, 1, 0, 1, 0, 0}, {0, 0, 1} <-> {1, 1, 1, 0, 0, 0}}, {{0, 0} <-> {1, 0, 0}, {1, 0, 0} <-> {0, 1}}]
Out[5]=

Show the abstract proof network:

In[6]:=
proof["ProofGraph"]
Out[6]=

Scope (2) 

Show that a list equivalence proposition cannot be derived from a given set of multiway system axioms:

In[7]:=
ResourceFunction["FindListProof"][{0} <-> {1, 0}, {0} <-> {0, 1}]
Out[7]=

Rules and Initial Conditions (2) 

FindListProof accepts both individual axioms and lists of axioms:

In[8]:=
ResourceFunction[
 "FindListProof"][{0, 0, 0} <-> {0, 0, 0, 0, 0, 0}, {0} <-> {0, 0}]
Out[8]=
In[9]:=
ResourceFunction[
 "FindListProof"][{0, 0, 0} <-> {0, 1, 0, 0, 1, 1}, {{0} <-> {0, 1}, {1} <-> {1, 0}}]
Out[9]=

Likewise for theorems:

In[10]:=
ResourceFunction[
 "FindListProof"][{{0, 0, 0} <-> {0, 1, 0, 0, 1, 1}, {0, 0, 0} <-> {0,
     0, 1, 0, 1, 0}}, {{0} <-> {0, 1}, {1} <-> {1, 0}}]
Out[10]=

Options (2) 

TimeConstraint (2) 

Use TimeConstraintt to limit the computation time to t seconds:

In[11]:=
ResourceFunction[
 "FindListProof"][{0, 0, 1, 0, 0} <-> {0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 1, 1, 1}, {{0} <-> {0, 1, 0}, {0, 0} <-> {1}}, TimeConstraint -> 0.01]
Out[11]=

By default, FindListProof looks for a proof indefinitely:

In[12]:=
ResourceFunction[
  "FindListProof"][{0, 0, 1, 0, 0} <-> {0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 1, 1, 1}, {{0} <-> {0, 1, 0}, {0, 0} <-> {1}}] // AbsoluteTiming
Out[12]=

Properties and Relations (1) 

FindListProof will return a proof object for a particular theorem if and only if the associated path exists in the corresponding multiway system:

In[13]:=
ResourceFunction[
 "FindListProof"][{0, 0, 1, 0, 0} <-> {0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 1, 1, 1}, {{0} <-> {0, 1, 0}, {0, 0} <-> {1}}]
Out[13]=
In[14]:=
mwGraph = ResourceFunction[
   "MultiwaySystem"][{{0} -> {0, 1, 0}, {0, 0} -> {1}}, {0, 0, 1, 0, 0}, 10, "StatesGraphStructure"]
Out[14]=
In[15]:=
path = FindShortestPath[
  mwGraph, {0, 0, 1, 0, 0}, {0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1,
    0, 1, 1, 1, 1}]
Out[15]=
In[16]:=
HighlightGraph[mwGraph, Subgraph[mwGraph, path]]
Out[16]=

Resource History

Source Metadata

Related Resources

License Information