nltk - Journey with the jar man

NLTK has some CRAZY (read: AWESOME) integration with automated theorem proving package: Prover9 (the successor of the Otter theorem prover, built on the "resolution concept" of mathematical logic). To understand resolution, one can read the incomprehensible wiki entry or the superior "wolfram" version, which PROPERLY attributes the technique to Yorkshire computer genius, John Alan Robinson, the "intellectual facilitator" of Prolog.