Wolfram Research

Function Repository Resource:

FindListProof

Source Notebook

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

Contributed by: Jonathan Gorard

ResourceFunction["FindListProof"][thm,axms]

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

Details and Options

If ResourceFunction["FindListProof"][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["FindListProof"] accepts both individual axioms and lists of axioms, and likewise for theorems.
ResourceFunction["FindListProof"] has the following option:
TimeConstraint Infinity how much time to allow
If ResourceFunction["FindListProof"] exceeds the specified time constraint, it returns a Failure object.
ResourceFunction["FindListProof"][thm,axms] uses the KnuthBendix 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 lists in a simple multiway system:

In[1]:=
proof = ResourceFunction[
  "FindListProof"][{0, 0} <-> {0, 1, 0, 1}, {0} <-> {0, 1}]
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[
  "FindListProof"][{{0, 0, 0} <-> {1, 1, 0, 1, 0, 0}, {0, 0, 1} <-> {1, 1, 1, 0, 0, 0}}, {{0, 0} <-> {1, 0, 0}, {1, 0, 0} <-> {0, 1}}]
Out[5]=

Show the abstract proof network:

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

Scope

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

In[7]:=
ResourceFunction["FindListProof"][{0} <-> {1, 0}, {0} <-> {0, 1}]
Out[7]=

Rules and Initial Conditions

FindListProof accepts both individual axioms and lists of axioms:

In[8]:=
ResourceFunction[
 "FindListProof"][{0, 0, 0} <-> {0, 0, 0, 0, 0, 0}, {0} <-> {0, 0}]
Out[8]=
In[9]:=
ResourceFunction[
 "FindListProof"][{0, 0, 0} <-> {0, 1, 0, 0, 1, 1}, {{0} <-> {0, 1}, {1} <-> {1, 0}}]
Out[9]=

Likewise for theorems:

In[10]:=
ResourceFunction[
 "FindListProof"][{{0, 0, 0} <-> {0, 1, 0, 0, 1, 1}, {0, 0, 0} <-> {0,
     0, 1, 0, 1, 0}}, {{0} <-> {0, 1}, {1} <-> {1, 0}}]
Out[10]=

Options

TimeConstraint

Use TimeConstraintt to limit the computation time to t seconds:

In[11]:=
ResourceFunction[
 "FindListProof"][{0, 0, 1, 0, 0} <-> {0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 1, 1, 1}, {{0} <-> {0, 1, 0}, {0, 0} <-> {1}}, TimeConstraint -> 0.01]
Out[11]=

By default, FindListProof looks for a proof indefinitely:

In[12]:=
ResourceFunction[
  "FindListProof"][{0, 0, 1, 0, 0} <-> {0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 1, 1, 1}, {{0} <-> {0, 1, 0}, {0, 0} <-> {1}}] // AbsoluteTiming
Out[12]=

Properties and Relations

FindListProof 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[
 "FindListProof"][{0, 0, 1, 0, 0} <-> {0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 1, 1, 1}, {{0} <-> {0, 1, 0}, {0, 0} <-> {1}}]
Out[13]=
In[14]:=
mwGraph = ResourceFunction[
   "MultiwaySystem"][{{0} -> {0, 1, 0}, {0, 0} -> {1}}, {0, 0, 1, 0, 0}, 10, "StatesGraphStructure"]
Out[14]=
In[15]:=
path = FindShortestPath[
  mwGraph, {0, 0, 1, 0, 0}, {0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1,
    0, 1, 1, 1, 1}]
Out[15]=
In[16]:=
HighlightGraph[mwGraph, Subgraph[mwGraph, path]]
Out[16]=

Resource History

Source Metadata

Related Resources

License Information