Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

Function Repository Resource:

 FindWolframModelProof

Source Notebook

Try to find a proof of equivalence between hypergraphs in a given multiway Wolfram model system

Contributed by: Jonathan Gorard

ResourceFunction["FindWolframModelProof"][thm,axms]

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

Details and Options

If ResourceFunction["FindWolframModelProof"][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["FindWolframModelProof"] accepts both individual axioms and lists of axioms, and likewise for theorems.
ResourceFunction["FindWolframModelProof"] has the following options:
TimeConstraintInfinityhow much time to allow
"DirectedHyperedges"Truewhether to treat hyperedges as being ordered (directed)
If ResourceFunction["FindWolframModelProof"] exceeds the specified time constraint, it returns a Failure object.
ResourceFunction["FindWolframModelProof"][thm,axms] uses the Knuth–Bendix completion algorithm to prove that the theorem thm follows from the axioms axms.

Examples

Basic Examples (3) 

Prove an elementary theorem regarding the equivalence of two hypergraphs in a simple multiway Wolfram model system:

In[1]:=
proof = ResourceFunction[ "FindWolframModelProof"][{{1, 2}} <-> {{1, 2}, {2, 4}, {2, 3}, {3, 5}}, {{x, y}} <-> {{x, y}, {y, z}}]
Out[1]=
Image

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

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

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

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

Typeset a natural language argument:

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

Prove a more sophisticated theorem involving multiple rules and hypotheses:

In[5]:=
proof = ResourceFunction[ "FindWolframModelProof"][{{{1, 1, 1}} <-> {{1, 1, 1}, {1, 2, 1}, {1, 1, 2}}, {{1, 1, 1}} <-> {{1, 2, 1}, {1, 1, 1}, {1, 3, 1}, {1, 1, 3}, {2, 2, 1}, {2, 4, 2}, {1, 2, 4}}}, {{{x, x, y}} <-> {{y, y, x}, {y, z, y}, {x, y, z}}, {{x, y, x}, {z, w, y}} <-> {{w, z, y}}}]
Out[5]=
Image

Show the abstract proof network:

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

Theorems that are true in the case of orderless (undirected) hyperedges may not be true in the case of ordered (directed) ones:

In[7]:=
ResourceFunction[ "FindWolframModelProof"][{{2, 1}} <-> {{1, 1}, {1, 2}}, {{x, y}} <-> {{x, x}, {x, y}}, TimeConstraint -> 5]
Out[7]=
Image
In[8]:=
ResourceFunction[ "FindWolframModelProof"][{{2, 1}} <-> {{1, 1}, {1, 2}}, {{x, y}} <-> {{x, x}, {x, y}}, TimeConstraint -> 5, "DirectedHyperedges" -> False]
Out[8]=
Image

Scope (4) 

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

In[9]:=
ResourceFunction[ "FindWolframModelProof"][{{0, 1}} <-> {{1, 2}}, {{x, y}} <-> {{y, x}}]
Out[9]=
Image

Rules and Initial Conditions (2) 

FindWolframModelProof accepts both individual axioms and lists of axioms:

In[10]:=
ResourceFunction[ "FindWolframModelProof"][{{1, 1, 1}} <-> {{1, 2, 1}, {1, 1, 1}, {1, 3, 1}, {1, 1, 3}, {2, 2, 1}, {2, 4, 2}, {1, 2, 4}}, {{x, x, y}} <-> {{y, y, x}, {y, z, y}, {x, y, z}}]
Out[10]=
Image
In[11]:=
ResourceFunction[ "FindWolframModelProof"][{{1, 1, 1}} <-> {{1, 2, 1}, {1, 1, 1}, {1, 3, 1}, {1, 1, 3}, {2, 2, 1}, {2, 4, 2}, {1, 2, 4}}, {{{x, x, y}} <-> {{y, y, x}, {y, z, y}, {x, y, z}}, {{x, y, x}, {z, w, y}} <-> {{w, z, y}}}]
Out[11]=
Image

Likewise for theorems:

In[12]:=
ResourceFunction[ "FindWolframModelProof"][{{{1, 1, 1}} <-> {{1, 2, 1}, {1, 1, 1}, {1, 3, 1}, {1, 1, 3}, {2, 2, 1}, {2, 4, 2}, {1, 2, 4}}, {{1, 1, 1}} <-> {{1, 1, 1}, {1, 2, 1}, {1, 1, 2}}}, {{{x, x, y}} <-> {{y, y, x}, {y, z, y}, {x, y, z}}, {{x, y, x}, {z, w, y}} <-> {{w, z, y}}}]
Out[12]=
Image

Types of Hyperedges (2) 

FindWolframModelProof supports single-vertex edges, ordered two-vertex edges (i.e. ordinary directed edges) and ordered three-vertex hyperedges:

In[13]:=
ResourceFunction[ "FindWolframModelProof"][{{1}, {2}} <-> {{1}, {5}, {3}, {6}, {2}, {7}, {4}, {8}}, {{x}} <-> {{x}, {y}}]
Out[13]=
Image
In[14]:=
ResourceFunction[ "FindWolframModelProof"][{{1, 2}} <-> {{1, 2}, {2, 4}, {2, 3}, {3, 5}}, {{x, y}} <-> {{x, y}, {y, z}}]
Out[14]=
Image
In[15]:=
ResourceFunction[ "FindWolframModelProof"][{{1, 2, 3}, {2, 3, 1}, {2, 3, 1}, {3, 1, 2}} <-> {{1, 2, 3}}, {{x, y, z}} <-> {{x, y, z}, {y, z, x}}]
Out[15]=
Image

As well as combinations of all three:

In[16]:=
ResourceFunction[ "FindWolframModelProof"][{{1, 2, 3}, {1, 3}} <-> {{1, 2, 3}, {2, 3, 1}, {1, 2}, {2, 3}, {3}}, {{x, y, z}, {x, z}} <-> {{x, y, z}, {y, z, x}, {x, y}, {y, z}, {z}}]
Out[16]=
Image

Options (4) 

TimeConstraint (2) 

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

In[17]:=
ResourceFunction[ "FindWolframModelProof"][{{1, 1, 1}} <-> {{1, 2, 1}, {1, 1, 1}, {1, 3, 1}, {1, 1, 3}, {2, 2, 1}, {2, 4, 2}, {1, 2, 4}}, {{x, x, y}} <-> {{y, y, x}, {y, z, y}, {x, y, z}}, TimeConstraint -> 0.01]
Out[17]=
Image

By default, FindWolframModelProof looks for a proof indefinitely:

In[18]:=
ResourceFunction[ "FindWolframModelProof"][{{1, 1, 1}} <-> {{1, 2, 1}, {1, 1, 1}, {1, 3, 1}, {1, 1, 3}, {2, 2, 1}, {2, 4, 2}, {1, 2, 4}}, {{x, x, y}} <-> {{y, y, x}, {y, z, y}, {x, y, z}}] // AbsoluteTiming
Out[18]=
Image

DirectedHyperedges (2) 

By default, all hyperedges are treated as ordered (i.e. directed):

In[19]:=
ResourceFunction[ "FindWolframModelProof"][{{2, 1}} <-> {{1, 1}, {1, 2}}, {{x, y}} <-> {{x, x}, {x, y}}, TimeConstraint -> 5]
Out[19]=
Image

Use "DirectedHyperedges"→False to treat all hyperedges as orderless (i.e. undirected):

In[20]:=
ResourceFunction[ "FindWolframModelProof"][{{2, 1}} <-> {{1, 1}, {1, 2}}, {{x, y}} <-> {{x, x}, {x, y}}, TimeConstraint -> 5, "DirectedHyperedges" -> False]
Out[20]=
Image

Properties and Relations (1) 

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

In[21]:=
ResourceFunction[ "FindWolframModelProof"][{{1, 2}} <-> {{1, 2}, {1, 3}, {4, 1}, {5, 4}}, {{x, y}} <-> {{x, y}, {y, z}}]
Out[21]=
Image
In[22]:=
mwGraph = ResourceFunction["MultiwaySystem"][ "WolframModel" -> {{{x, y}} -> {{x, y}, {y, z}}}, {{{1, 2}}}, 3, "StatesGraphStructure"]
Out[22]=
Image
In[23]:=
path = FindShortestPath[ mwGraph, {{1, 2}}, {{1, 2}, {1, 3}, {4, 1}, {5, 4}}]
Out[23]=
Image
In[24]:=
HighlightGraph[mwGraph, Subgraph[mwGraph, path]]
Out[24]=
Image

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