riceissa
commented
5 years ago I think this is basically the difference between the two proofs of Proposition A.3.1 and A.3.2 in Tao's Analysis I. i.e. instead of going:
- A
- A → C
- C
- C → D
- D
- D → B
- B
we go:
- D → B
- C → D
- A → C
- A
- C
- D
- B
In other words, we backchain from what we need (B) to what we have (A).
I'm searching both "premise selection" and "premiss selection" but can't find a page that explains this (it's mentioned in a bunch of papers).