A similar book to Concrete Semantics, which I love, is Formal Reasoning about Programs by the same group the OP link comes from: http://adam.chlipala.net/frap/f

A similar book to Concrete Semantics, which I love, is Formal Reasoning about Programs by the same group the OP link comes from: http://adam.chlipala.net/frap/frap_book.pdf http://adam.chlipala.net/frap/frap_book.pdf ML for the Working Programmer is written by Paulson, one of the main persons behind Isabelle, and ends up with a prover project: https://www.cl.cam.ac.uk/~lp15/MLbook/ https://www.cl.cam.ac.uk/~lp15/MLbook/ Paulson teaches an undergrad course in Cambridge which is now using Huth & Ryan as a textbook. It's an incredible book that focuses on logic, SAT solvers and model checking. Probably the place to begin. An incomplete draft 2nd edition is in the authors website: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/tmp/Anongporn/Ch1+3.pdf If you are interested in tableaux techniques, First-order Logic and Automated Theorem Proving by Fitting is a good text. Personally, I think the place to start from is Huth & Ryan. Logic is the calculus of CS. Then progress to type theory using a book like TAPL by Pierce or Proofs and Types by Girard. Then, depending on your interests, you can proceed to model checking, program analysis and theorem proving. For the first two, the classics are Katoen and Nielson & Nielson, respectively.