Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

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:
TimeConstraintInfinityhow much time to allow
If ResourceFunction["FindListProof"] exceeds the specified time constraint, it returns a Failure object.
ResourceFunction["FindListProof"][thm,axms] uses the Knuth–Bendix 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 TimeConstraint→t 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]=

Publisher

Jonathan Gorard

Version History

  • 1.0.0 – 03 August 2020

Source Metadata

  • Citation:
    • Stephen Wolfram (2002), A New Kind of Science.
    • Stephen Wolfram (2020), "A Class of Models with the Potential to Represent Fundamental Physics".
    • Jonathan Gorard (2020), "Some Relativistic and Gravitational Properties of the Wolfram Model".
    • Jonathan Gorard (2020), "Some Quantum Mechanical Properties of the Wolfram Model".

Related Resources

License Information