Wolfram Research

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:
TimeConstraint Infinity how much time to allow
"DirectedHyperedges" True whether 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

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]=

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[
  "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]=

Show the abstract proof network:

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

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

Scope

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]=

Rules and Initial Conditions

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]=
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]=

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]=

Types of Hyperedges

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]=
In[14]:=
ResourceFunction[
 "FindWolframModelProof"][{{1, 2}} <-> {{1, 2}, {2, 4}, {2, 3}, {3, 5}}, {{x, y}} <-> {{x, y}, {y, z}}]
Out[14]=
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]=

It also accepts 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]=

Options

TimeConstraint

Use TimeConstraintt 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]=

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]=

DirectedHyperedges

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]=

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]=

Properties and Relations

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

Resource History

Source Metadata

Related Resources

License Information