 | |
| |
Handbook of Automated Reasoning
 |
Author: J. Alan Robinson, Andrei Voronkov
List Price: $130.00
Our Price: Click to see the latest and low price
ISBN: 0262182211
Publisher: MIT Press (01 September, 2001)
Edition: Hardcover
Sales Rank: 1,203,943
Average Customer Rating: 4 out of 5
|
Customer ReviewsRating: 4 out of 5
Required reading for ATP researchers
I've found this to be the best introduction to (mostly classical) automated theorem proving. The matter is clearly presented and can be understood even by non-logicians. In the first part of the book there is a solid treatment of classical theorem proving, including an excellent chapter on tableau based methods. In the second part there is a short treatment of intuitionistic theorem proving, and some throwaway discussion of the relation of theorem proving and type-theory (specifically, dependent type-theories as used in Logical Frameworks), model checking, verification, etc. I give the book 4 stars because of its well-rounded discussion of classical theorem proving, and hold back the last star because the material is a bit dated compared to modern research directions, and doesn't cover intuitionistic theorem proving in great detail.
| | | | | |
| |
