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

"The following sentence is a substitution axiom for the binary relation constant
q. Note that we need to allow for equations for all of the arguments of 
relational sentences.

     Au:Av:Ax:Ay:(q(u,v) & u=x & v=y => q(x,y))"

In my system, I don't need another axiom; substitution is built in to the program:

---

C:\logicagent>ruby logicbot.rb
Hello
I have loaded C:/logicagent/logicagent-api.yaml.
C:/logicagent/graph.yaml loaded.

> reset graph
Okay, I have reset the graph.

> John is older than William.
Okay, John is older than William.

> John = Jack
Okay, John = Jack.

> William = Bill
Okay, William = Bill.

> is Jack older than Bill?
Yes, Jack is older than Bill.

>

---

The program can do substitution without needing another axiom.