Analysing mathematical proofs (or reading between the lines)

John Wiley and Sons, Inc. Robinson, J.A. (1965) "A Machine Oriented Logic Based on the Resolution Principle".