I’m going to list various types of backward chaining, along with implementations that follow a given type

WAM (Warren’s Abstract Machine)
- most Prologs…
TOAM (Tree-Oriented Abstract Machine)
- B-Prolog
Specialized (backward and forward chaining on the same structure)
- JESS – Built on top of a Rete network
- CLIPS/R2 – Uses ‘Rete II’, which adds backward chaining and hashed memories

Not sure yet
- Mandarax – contains implementations of 4 inference engines, at least one of which is backward chaining
- Eulersharp – “backward-chaining reasoner enhanced with Euler path detection”