From Notes to Coursera/Stanford's Introduction to Philosophy, Chapter 9: Equality:
----------------------------------------------------------------------------------

From Section 9.4:
-----------------

"The following is a proof of the result in Section 9.2 using these extensions 
in lieu of the equality axioms. Note that with these rules we can do the proof 
in a single step.

     1. b=a     Premise
     2. b=c     Premise
     3. a=c     Equality Elimination 2,1"

The proof in Section 9.2 looks something like:

---
1.		b=a		Premise
2.		b=c		Premise
3.		Ax.x=x		Reflexivity
4.		Ax.Ay.(x=y => y=x)		Symmetry
5.		Ax.Ay.Az.(x=y & y=z => x=z)		Transitivity
6.		b=a => a=b		2×UE: 4
7.		a=b		IE: 6, 1
8.		a=b & b=c ? a=c		3×UE: 5
9.		a=b & b=c		And Introduction: 7, 2
10.		a=c		IE: 8, 9

---

In my system, I can also do this proof in 3 steps (including the Premises):

---

> reset graph
Okay, I have reset the graph.

> b=a
Default response.

> b = a
Okay, b = a.

> b = c
Okay, b = c.

> does a = c?
Yes, a = c.

>

---

Note that I have to include spaces delimiting the object constants.

However, I want the bot to be flexible, customizable. So, I can tell it, 
via a rule submitted at runtime, to make "b=a" into "b = a":

---

> reset graph
Okay, I have reset the graph.

> logicbot: if input =~ /([a-zA-Z]+)=([a-zA-Z]+)/ then response = self.send("#{$1} = #{$2}") end
Okay I have added if input =~ /([a-zA-Z]+)=([a-zA-Z]+)/ then response = self.send("#{$1} = #{$2}") end.

> b=a
Okay, b = a.

> b=c
Okay, b = c.

> does a = c?
Yes, a = c.

>