In[]:=

FindEquationalProof[b==(a∘b)∘b,ForAll[{a,b},a∘b==b]]

Out[]=

ProofObject

In[]:=

FindEquationalProof[b==(a∘b)∘b,ForAll[{a,b},a∘b==b]]["ProofDataset"]

Out[]=

In[]:=

FindEquationalProof[b==(a∘b)∘b,ForAll[{a,b},a∘b==b]]["ProofGraph"]

Out[]=

FindEquationalProof[b==(a∘b)∘b,ForAll[{a,b},a∘b==b]]["ProofGraph"]

In[]:=

AccumulativeTokenEventGraph[{a_<->b_∘a_},1,"SC"]

Out[]=

In[]:=

DeleteCases[VertexList[AccumulativeTokenEventGraph[{a_<->b_∘a_},1,"SC"],_TwoWayRule]/.p_Pattern:>First[p]/.TwoWayRule->Equal,True]

Out[]=

{ab∘a,aa∘a,ab∘(b∘a),ab∘(c∘a),a(b∘a)∘a,a(b∘c)∘a,a∘bc∘b}

In[]:=

FindEquationalProof[#,ForAll[{a,b},a∘b==b]]["ProofGraph"]&/@%

Out[]=

,

,

,

,

,

,

In[]:=

FindEquationalProof[ab∘(b∘a),ForAll[{a,b},a∘b==b]]["ProofDataset"]

Out[]=

In[]:=

FindEquationalProof[ab∘(b∘a),ForAll[{a,b},a∘b==b]]["ProofNotebook"]

Out[]=

In[]:=

With[{g=AccumulativeTokenEventGraph[{a_<->b_∘a_},1,"SC","TokenLabeling"->True]},Subgraph[g,#]&/@findProof[g,{a_<->b_∘a_},a_<->b_∘(b_∘a_)]]

Out[]=

In[]:=

With[{g=AccumulativeTokenEventGraph[{a_<->b_∘a_},2,"S","TokenLabeling"->True]},Subgraph[g,#]&/@findProof[g,{a_<->b_∘a_},a_<->b_∘(b_∘a_)]]

Out[]=

Missing

In[]:=

AccumulativeTokenEventGraph[{a_<->b_∘a_,a_<->b_∘(b_∘a_)},1,"S"]

Out[]=

In[]:=

AccumulativeTokenEventGraph[{a_<->b_∘a_,a_<->b_∘(b_∘a_)},1,"S","TokenLabeling"->True]

Out[]=

In[]:=

VertexList[%,_TwoWayRule]

#### Objective of theorem proving: find at least one of the axioms and the hypothesis [and nothing else] in the past entailment cone of “True”

Objective of theorem proving: find at least one of the axioms and the hypothesis [and nothing else] in the past entailment cone of “True”

#### Restatement: we’re looking for an overlap (i.e. a=a) in the past entailment cone of the hypothesis, and the future one of the axioms

Restatement: we’re looking for an overlap (i.e. a=a) in the past entailment cone of the hypothesis, and the future one of the axioms

#### [If we’re dealing with expressions, we just have to extend the path ... to reach from the future cone of the axioms into the past cone of the hypothesis]

[If we’re dealing with expressions, we just have to extend the path ... to reach from the future cone of the axioms into the past cone of the hypothesis]

## More theorems

More theorems

### Confluence in our model??

Confluence in our model??

#### Predicate logic?

Predicate logic?