Function Repository Resource:

# FindWolframModelProof

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 (3)

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

 In[1]:=
 Out[1]=

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

 In[2]:=
 Out[2]=

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

 In[3]:=
 Out[3]=

Typeset a natural language argument:

 In[4]:=
 Out[4]=

Prove a more sophisticated theorem involving multiple rules and hypotheses:

 In[5]:=
 Out[5]=

Show the abstract proof network:

 In[6]:=
 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]:=
 Out[7]=
 In[8]:=
 Out[8]=

### Scope (4)

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

 In[9]:=
 Out[9]=

#### Rules and Initial Conditions (2)

FindWolframModelProof accepts both individual axioms and lists of axioms:

 In[10]:=
 Out[10]=
 In[11]:=
 Out[11]=

Likewise for theorems:

 In[12]:=
 Out[12]=

#### 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]:=
 Out[13]=
 In[14]:=
 Out[14]=
 In[15]:=
 Out[15]=

As well as combinations of all three:

 In[16]:=
 Out[16]=

### Options (4)

#### TimeConstraint (2)

Use to limit the computation time to t seconds:

 In[17]:=
 Out[17]=

By default, FindWolframModelProof looks for a proof indefinitely:

 In[18]:=
 Out[18]=

#### DirectedHyperedges (2)

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

 In[19]:=
 Out[19]=

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

 In[20]:=
 Out[20]=

### 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]:=
 Out[21]=
 In[22]:=
 Out[22]=
 In[23]:=
 Out[23]=
 In[24]:=
 Out[24]=

Jonathan Gorard

## Version History

• 1.0.0 – 03 August 2020