Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

Function Repository Resource:

 FindStringProof

Source Notebook

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

Contributed by: Jonathan Gorard

ResourceFunction["FindStringProof"][thm,axms]

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

Details and Options

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

Examples

Basic Examples (2) 

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

In[1]:=
proof = ResourceFunction["FindStringProof"]["AA" <-> "ABAB", "A" <-> "AB"]
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[ "FindStringProof"][{"AAA" <-> "BBABAA", "AAB" <-> "BBBAAA"}, {"AA" <-> "BAA", "BAA" <-> "AB"}]
Out[5]=

Show the abstract proof network:

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

Scope (2) 

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

In[7]:=
ResourceFunction["FindStringProof"]["A" <-> "C", "A" <-> "B"]
Out[7]=

Rules and Initial Conditions (2) 

FindStringProof accepts both individual axioms and lists of axioms:

In[8]:=
ResourceFunction["FindStringProof"]["AAA" <-> "AAAAAA", "A" <-> "AA"]
Out[8]=
In[9]:=
ResourceFunction["FindStringProof"][ "AAA" <-> "ABAABB", {"A" <-> "AB", "B" <-> "BA"}]
Out[9]=

Likewise for theorems:

In[10]:=
ResourceFunction[ "FindStringProof"][{"AAA" <-> "ABAABB", "AAA" <-> "AABABA"}, {"A" <-> "AB", "B" <-> "BA"}]
Out[10]=

Options (2) 

TimeConstraint (2) 

Use TimeConstraint→t to limit the computation time to t seconds:

In[11]:=
ResourceFunction["FindStringProof"][ "AABAA" <-> "ABABABABABABABABBBB", {"A" <-> "ABA", "AA" <-> "B"}, TimeConstraint -> 0.01]
Out[11]=

By default, FindStringProof looks for a proof indefinitely:

In[12]:=
ResourceFunction["FindStringProof"][ "AABAA" <-> "ABABABABABABABABBBB", {"A" <-> "ABA", "AA" <-> "B"}] // AbsoluteTiming
Out[12]=

Properties and Relations (1) 

FindStringProof 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["FindStringProof"][ "AABAA" <-> "ABABABABABABABABBBB", {"A" <-> "ABA", "AA" <-> "B"}]
Out[13]=
In[14]:=
mwGraph = ResourceFunction["MultiwaySystem"][{"A" -> "ABA", "AA" -> "B"}, "AABAA", 10, "StatesGraphStructure"]
Out[14]=
In[15]:=
path = FindShortestPath[mwGraph, "AABAA", "ABABABABABABABABBBB"]
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