This book meets the demand for a self-contained and broad-based account of the concepts, the machinery and the use of automated reasoning. The mathematical logic foundations are described in conjunction with practical application, all with the minimum of prerequisites. The approach is constructive, concrete and algorithmic: a key feature is that methods are described with reference to actual implementations (for which code is supplied) that readers can use, modify and experiment with. This book is ideally suited for those seeking a one-stop source for the general area of automated reasoning. It can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study.
FREE Two-Day Shipping for students on millions of items. Learn more |
 Sell Back Your Copy for $11.00
Whether you buy it used on Amazon for $117.53 or somewhere else, you can sell it back through our Book Trade-In Program at the current price of $11.00.
Used Price$117.53
Trade-in Price$11.00
Price after
Trade-in$106.53 |
Book Description
Frequently Bought Together
Editorial Reviews
Review
"Valuable as both a strong introduction for complete beginners and a rich reference source, even for expert logicians."
D.V. Feldman, CHOICE
" [...] if you want to implement ATP (automated theorem proving) code this book is an excellent choice. It has complete implementations of absolutely everything in OCaml (a dialect of ML, a mostly functional programming language) which is an excellent choice for this type of application."
D. Fox, amazon.com
"[...] sure to fill a need for a well-rounded work that can serve both as a reference on a range of topics and as an introductory text, especially for those who wish to study the subject for its possible practical uses. [...] Good features of the book are its overall readability, the good historical perspective conveyed while retaining its serious scholarly gravitas, and the use of OCaml to work with the concepts, presented alongside."
Shrisha Rao, Computing Reviews
"Harrison exhibits both the remarkable flexibility and limitations of OCaml (and other languages) for automated theorem proving. [...] I strongly recommend Harrison's handbook to mathematicians working on provability, computer program developers working to establish self-coherence of some parts of their programs, and students looking to understand propositional and first-order logic."
Arturo Ortiz-Tapia, Computing Reviews
"[...] the book is remarkable in many ways, including the breadth of its scope, the depth of its insights, and the clarity and readability of its prose. [...] while Harrison does focus on implementation and practical issues, he does not skimp on the underlying theory; indeed, the text passes between the two poles with surprising fluidity. The book does not assume background in logic, and appendices review the requisite background in mathematics and programming. As a result, the text is accessible to a broad audience, including sufficiently advanced undergraduates. [...] Harrison does a very good job of providing broader context and pointers to the literature. Each section ends with copious notes and references. As a result, the book can serve as a helpful introduction to the contemporary literature, like having a friendly uncle working in the field. [...] It provides a lucid and synoptic overview of these topics, conveys a solid theoretical background, provides tools for experimentation, and offers notes and pointers that facilitate a smooth transition to the contemporary literature. [...] Anyone working in automated reasoning, or looking to come up to speed on developments in the field, will want to have a copy at hand."
Jeremy Avigad, Theory and Practice of Logic Programming
"Overall this is an excellent book that provides a wide-ranging view on automated reasoning techniques for classical logic. The author achieves a good balance between providing good intuition and rigour in presenting the selected materials. Its breadth will make sure that even an expert in the area will find something useful in the book."
Alwen Tiu, The Bulletin of Symbolic Logic
D.V. Feldman, CHOICE
" [...] if you want to implement ATP (automated theorem proving) code this book is an excellent choice. It has complete implementations of absolutely everything in OCaml (a dialect of ML, a mostly functional programming language) which is an excellent choice for this type of application."
D. Fox, amazon.com
"[...] sure to fill a need for a well-rounded work that can serve both as a reference on a range of topics and as an introductory text, especially for those who wish to study the subject for its possible practical uses. [...] Good features of the book are its overall readability, the good historical perspective conveyed while retaining its serious scholarly gravitas, and the use of OCaml to work with the concepts, presented alongside."
Shrisha Rao, Computing Reviews
"Harrison exhibits both the remarkable flexibility and limitations of OCaml (and other languages) for automated theorem proving. [...] I strongly recommend Harrison's handbook to mathematicians working on provability, computer program developers working to establish self-coherence of some parts of their programs, and students looking to understand propositional and first-order logic."
Arturo Ortiz-Tapia, Computing Reviews
"[...] the book is remarkable in many ways, including the breadth of its scope, the depth of its insights, and the clarity and readability of its prose. [...] while Harrison does focus on implementation and practical issues, he does not skimp on the underlying theory; indeed, the text passes between the two poles with surprising fluidity. The book does not assume background in logic, and appendices review the requisite background in mathematics and programming. As a result, the text is accessible to a broad audience, including sufficiently advanced undergraduates. [...] Harrison does a very good job of providing broader context and pointers to the literature. Each section ends with copious notes and references. As a result, the book can serve as a helpful introduction to the contemporary literature, like having a friendly uncle working in the field. [...] It provides a lucid and synoptic overview of these topics, conveys a solid theoretical background, provides tools for experimentation, and offers notes and pointers that facilitate a smooth transition to the contemporary literature. [...] Anyone working in automated reasoning, or looking to come up to speed on developments in the field, will want to have a copy at hand."
Jeremy Avigad, Theory and Practice of Logic Programming
"Overall this is an excellent book that provides a wide-ranging view on automated reasoning techniques for classical logic. The author achieves a good balance between providing good intuition and rigour in presenting the selected materials. Its breadth will make sure that even an expert in the area will find something useful in the book."
Alwen Tiu, The Bulletin of Symbolic Logic
Book Description
A self-contained and broad-based account of the concepts, the machinery and the use of automated reasoning. It's ideal for those seeking a one-stop source for the subject. The approach is constructive, concrete and algorithmic: importantly, methods are described with reference to actual implementations (for which code is supplied).
Product Details
Would you like to update product info or give feedback on images?
|
More About the Author
Discover books, learn about writers, read author blogs, and more.
Customer Reviews
|
Share your thoughts with other customers:
|
||||||||||||||||||||||
|
Most Helpful Customer Reviews
3 of 3 people found the following review helpful:
5.0 out of 5 stars
The Best Choice for learning ATP,
By
Amazon Verified Purchase(What's this?)
This review is from: Handbook of Practical Logic and Automated Reasoning (Hardcover)
I've only just received this book, but after a few hours I can say that if you want to implement ATP (automated theorem proving) code this book is an excellent choice. It has complete implementations of absolutely everything in OCaml (a dialect of ML, a mostly functional programming language) which is an excellent choice for this type of application. Almost as good as Haskell (I kid.) Chang and Lee is a great book, but forty years have passed...
2 of 2 people found the following review helpful:
5.0 out of 5 stars
The most complete and enjoyable book on ATP,
By Georg (Princeton, NJ) - See all my reviews
This review is from: Handbook of Practical Logic and Automated Reasoning (Hardcover)
This book is an excellent introduction into the world of automated theorem proving. The author takes it slowly, building up from the very basics, but the book is still very complete and covers most relevant topics (with the exception of modern SMT solvers, perhaps, which only get a rather meagre coverage -- I'd recommend Kroening and Strichman's book on decision procedures as a complement to Harrison's book). Harrison's book is also complete in the sense that there's an implementation for _every_ algorithm described in this book (so, you'll have a hard time finding a handwavy description). Some people might frown upon the use of OCaml instead of a more widely used language like C++ or Java, but, let's be honest, nobody wants to read pages of source code and class definitions if there's a programming language which is designed for the job and can describe ATP algorithms much more succinctly. While reading the book you can basically build your own automated theorem prover from scratch. The disadvantage of this approach is that, if you just want to read up on some more sophisticated decision procedures, you'll more often than not find yourself looking up the implementation of certain basic functions in the earlier chapters of the book. Keep that in mind if you want to use the book as a reference rather than as a tutorial (I'm not saying that it can't be used as a reference, however, it can sometimes turn out to be a bit time-consuming to look up things). Finally, I really like Harrison's writing style. It's always a joy to read this book, and it's very much to the point and never over-burdened (but there are many cross-references if you want to dig deeper). This book is a 'must-have' for everyone who's interested in automated decision procedures.
3.0 out of 5 stars
A good, but very expensive book similar to two other books,
By Scott (Dubuque, IA) - See all my reviews
This review is from: Handbook of Practical Logic and Automated Reasoning (Hardcover)
THIS BOOK
I have not quite ever purchased this book by John Harrison and will not now that its list price has increased from $150 to $165, with Amazon's price increasing accordingly. When this book was more open for viewing in Amazon, it appeared quite good as a general logic text, but I would not benefit at all from all that OCaml code everywhere, and have no need to do automated theorem proving. THE SCHEME ALTERNATIVE In fact, I am currently about to learn some programming in Scheme instead of in OCaml. Scheme is recently freely available from MIT/GNU compiled for my Mac OS 10.6 operating system, with programming in the X11 Mac utility app. Windows and UNIX versions of Scheme have been available for much longer. TWO CROSS-TALKING BOOKS My main point from this Harrison textbook's contents is that the following two books I already own seem to have moderate cross-talk with the present 702 pager. Here are the links to those two Springer books: The Calculus of Computation: Decision Procedures with Applications to Verification / Mathematical Logic for Computer Science, and with a previous much different out of print book on this subject, which I also have: Logic for Computer Science: Foundations of Automatic Theorem Proving. I plan to read in the Calculus of Computation book in 2012.
Share your thoughts with other customers: Create your own review
|
|
Inside This Book
(learn more)
First Sentence:
In this chapter we introduce logical reasoning and the idea of mechanizing it, touching briefly on important historical developments. Read the first page Key Phrases - Statistically Improbable Phrases (SIPs): (learn more)
let fvs, vars sgns, vars poll, solve env, fixpoint lemma, functional reflexive axioms, stable infiniteness, component decision procedures, other binary connectives, connection tableaux, refutation completeness, let eqs, positive hyperresolution, minimal unsatisfiable subset, fol formula, combining decision procedures, quantifier elimination procedure, let cls, canonical term rewriting system, quantified subformulas, unsatisfiable set, limitative results, interactive theorem proving, weak confluence, finite model property Key Phrases - Capitalized Phrases (CAPs): (learn more)
Proof One, Proof Suppose, Davis Putnam, Mechanizing Herbrand, Fundamental Theorem of Algebra, Santa Claus, Proof First, Proof Let, Axiom of Choice, Using Theorem, Nelson Oppen, Principia Mathematica Browse Sample Pages:
Front Cover | Table of Contents | First Pages | Index | Surprise Me!
In this chapter we introduce logical reasoning and the idea of mechanizing it, touching briefly on important historical developments. Read the first page Key Phrases - Statistically Improbable Phrases (SIPs): (learn more)
let fvs, vars sgns, vars poll, solve env, fixpoint lemma, functional reflexive axioms, stable infiniteness, component decision procedures, other binary connectives, connection tableaux, refutation completeness, let eqs, positive hyperresolution, minimal unsatisfiable subset, fol formula, combining decision procedures, quantifier elimination procedure, let cls, canonical term rewriting system, quantified subformulas, unsatisfiable set, limitative results, interactive theorem proving, weak confluence, finite model property Key Phrases - Capitalized Phrases (CAPs): (learn more)
Proof One, Proof Suppose, Davis Putnam, Mechanizing Herbrand, Fundamental Theorem of Algebra, Santa Claus, Proof First, Proof Let, Axiom of Choice, Using Theorem, Nelson Oppen, Principia Mathematica Browse Sample Pages:
Front Cover | Table of Contents | First Pages | Index | Surprise Me!
What Other Items Do Customers Buy After Viewing This Item?
Tags Customers Associate with This Product(What's this?)Click on a tag to find related items, discussions, and people.
|
Sell a Digital Version of This Book in the Kindle Store
If you are a publisher or author and hold the digital rights to a book, you can sell a digital version of it in our Kindle Store.
Learn more
Customer Discussions
|
This product's forum
Active discussions in related forums
Search Customer Discussions
|
Related forums
|
Listmania!
|
|
So You'd Like to...
Look for Similar Items by Category
- Books > Computers & Technology > Computer Science > Artificial Intelligence
- Books > Computers & Technology > Programming > Languages & Tools
- Books > Health, Fitness & Dieting > Psychology & Counseling
- Books > New & Used Textbooks > Computer Science > Programming Languages
- Books > New & Used Textbooks > Humanities > Philosophy
- Books > Politics & Social Sciences > Philosophy
