In[]:=
FindEquationalProof[b==(a∘b)∘b,ForAll[{a,b},a∘b==b]]
Out[]=
ProofObject
Logic: EquationalLogic
Steps: 3
Theorem: b(a∘b)∘b

In[]:=
FindEquationalProof[b==(a∘b)∘b,ForAll[{a,b},a∘b==b]]["ProofDataset"]
Out[]=
Statement
Proof
Axiom
1
ab∘a
Hypothesis
1
(a∘b)∘bb
Conclusion
1
True
6 total ›
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[]=
{ab∘a,aa∘a,ab∘(b∘a),ab∘(c∘a),a(b∘a)∘a,a(b∘c)∘a,a∘bc∘b}
In[]:=
FindEquationalProof[#,ForAll[{a,b},a∘b==b]]["ProofGraph"]&/@%
Out[]=

,
,
,
,
,
,

In[]:=
FindEquationalProof[ab∘(b∘a),ForAll[{a,b},a∘b==b]]["ProofDataset"]
Out[]=
Statement
Proof
Axiom
1
ab∘a
Hypothesis
1
b∘(b∘a)a
SubstitutionLemma
1
b∘aa
6 total ›
Conclusion
1
True
6 total ›
In[]:=
FindEquationalProof[ab∘(b∘a),ForAll[{a,b},a∘b==b]]["ProofNotebook"]
Out[]=
Axiom 1
We are given that:
ab∘a
Hypothesis 1
We would like to show that:
b∘(b∘a)a
Substitution Lemma 1
It can be shown that:
b∘aa
Proof
We start by taking Hypothesis 1, and apply the substitution:
a_∘b_b
which follows from Axiom 1.
Conclusion 1
We obtain the conclusion:
True
Proof
Take Substitution Lemma 1, and apply the substitution:
a_∘b_b
which follows from Axiom 1.
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]
Out[]=
{a_b_∘a_,a_b_∘(b_∘a_),a_a_,a_b_∘(b_∘(c_∘a_)),a_b_∘(b_∘(c_∘(c_∘a_))),a_b_∘(c_∘a_),a_b_∘(c_∘(b_∘a_)),a_b_∘(c_∘(c_∘a_)),a_b_∘(c_∘(c_∘(b_∘a_))),a_b_∘((c_∘b_)∘a_),a_b_∘((c_∘(c_∘b_))∘a_),a_(b_∘c_)∘a_,a_(b_∘c_)∘(c_∘a_),a_(b_∘(b_∘c_))∘a_,a_(b_∘(b_∘c_))∘(c_∘a_),a_∘b_c_∘b_,a_∘b_c_∘(c_∘b_),a_∘(a_∘b_)c_∘b_,a_∘(a_∘b_)c_∘(c_∘b_)}

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

[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

Confluence in our model??

Predicate logic?