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.
>