Comment by jimsmart

"Divide and conquer recursive implementation" - so is that backward-chaining inference then? Or something different?

https://en.wikipedia.org/wiki/Backward_chaining