An automated theorem prover - where to start?
I am a second year student with my 2 discrete math assignment to do an automatic theorem check. I have to make a simple program that works in Propositional Logic in 4 weeks (assuming the proof always exists). So far I have searched google but the stuff is very difficult to understand after 4 weeks. Can anyone recommend me any book / site / open source for beginners or some helpful hints? Thank you in advance.
source to share
Note. I pointed out that this needs to be moved to the Computer Science site because they are so much more at the top of the ATP.
It would be nice if you could include what you looked at and why it doesn't help you. Then we can figure out what might be best for you. Also, if you need to write a program, knowing which languages you know will help. Most of what I do with this is done in a functional language like OCaml or F #, or in a logical language like Prolog or Mercury.
You've seen John Harrison's A Handbook of Practical Logic and Automated Reasoning (WorldCat) . I've included a link (WorldCat) so you can find the book in your local library rather than waiting for a purchase that will eat up most of your time.
If you look, you'll find OCaml code at the bottom of the page, and F # here and Haskell here .
If you don't see the ATP or Verification Assistant on Wikipedia, you might get some code and documents.
source to share