Preface; Ideological orientation; Acknowledgements; How to read this book; 1. Introduction; 2. Propositional logic; 3. First-order logic; 4. Equality; 5. Decidable problems; 6. Interactive theorem proving; 7. Limitations; Appendix 1. Mathematical background; Appendix 2. OCaml made light of; Appendix 3. Parsing and printing of formulas; References; Index.
A one-stop reference, self-contained, with theoretical topics presented in conjunction with implementations for which code is supplied.
John Harrison is a Principal Engineer at the Intel Corporation in Portland, Oregon. He specialises in formal verification, automated theorem proving, floating-point arithmetic and mathematical algorithms.
'Contemporary research in computer science has produced an
abundance of formal methods designed to enable hardware and
software systems to reason correctly, and to enable us to reason
better about these systems. Indeed, the explosion of research and
specialised techniques can make it hard for students and newcomers
to enter the field. John Harrison's Handbook of Practical Logic and
Automated Reasoning is a significant addition to the expository
literature on the subject, and will serve as a valuable resource
for beginners and experts alike.' Theory and Practice of Logic
Programming
'John Harrison … has written what clearly will be the book about
automation in theorem proving. People often ask me whether they
should buy this book. My answer … always is: yes, of course you
should buy this book. It is a masterpiece.' Journal of Automated
Reasoning
|
Ask a Question About this Product More... |
|
