Details

Change the value of "string to find" to see different proofs that go from the initial string to the selected string. Select "3D graph" to allow for a different view of the generated proofs (when they are complex enough).

It is usually a good idea to keep "max seconds" (the maximum amount of seconds before time out) and "max depth" to 2 and 6, respectively. For slower computers, "max seconds" could be increased. If you want to look for strings that are deeper than a depth of 6, you might want to set the depth to a larger value (8 is usually nice, though much slower) and to increase "max seconds" as much as that change could require.

On page 778 of the NKS book, S. Wolfram explains that this specific string rewriting system generates all strings; however, in this Demonstration many strings are not found because of the practical limits of time and memory of the search here.

This Demonstration is related to the research project developed at the NKS Summer School 2008 (NKS|Online), on proof sizes and lemmas in Wolfram's model of logic.