I want to learn automated theorem proving for use in a conversational agent. Although I have found a multitude of information using [google], I don't think I am qualified enough to choose what to read. Till now, I found this PDF draft... Plus, what does Prolog have to do with what I am trying to learn. Is it the thing am trying to implement, or does it help in implementing it... How much time do you think it will take to learn such a vast subject. I am an Electrical Engineering student who has just finished first year :), and I have a lot of programming knowledge under my belt (I think).

Prolog is a programming language that is to implement a lot of theorem provers. If you're serious about this, I suggest learning Prolog. Try reading these notes from my university.

Well, Ive looked at it quickly, and that PDF draft does contains all you need to implement a theorem prover in your favorite language. Prolog and LISP are probably the most appropriate. If you cant understand that PDF, then Im afraid you will need a stronger math background.

I would like to add CLIPS to the list too.

Prolog contains a backward-chaining inference engine
CLIPS contains a forward-chaining inference engine
LISP is a list-based language that allows to easily write recursive programs

Everyone choose his/her prefered language. Personnaly I go for python with puCLIPS module.

For complex theorem finding/proving, you may be interested in Douglas Lenat's works with Automated Mathematicians and Eurisko.