The logical systems presented are: propositional logic, first-order logic, resolution and its application to logic programming, Hoare logic for the verification of sequential programs, and linear temporal logic
for the verification of concurrent programs.
The third edition has been entirely rewritten and includes new chapters on central topics of modern computer science: SAT solvers and model checking.
The logical systems presented are:
- Propositional calculus (including binary decision diagrams);
- Predicate calculus;
- Hoare logic;
- Temporal logic.
Answers to exercises (for instructors only) as well as Prolog source code for algorithms may be found via the Springer London web site: http://www.springer.com/978-1-85233-319-5
Mordechai Ben-Ari is an associate professor in the Department of Science Teaching of the Weizmann Institute of Science. He is the author of numerous textbooks on concurrency, programming languages and logic, and has developed software tools for teaching concurrency. In 2004, Ben-Ari received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education.
The Spin model checker is not only a widely used professional tool but it is also a superb tool for teaching important concepts of computer science such as verification, concurrency and nondeterminism. The book introduces Spin-based software that the author has developed for teaching: jSpin - an integrated development environment for Spin; SpinSpider - uses output from Spin to automatically construct state diagrams of concurrent programs; VN is a tool for visualizing nondeterminism.
Complete programs will demonstrate each construct and concept and these programs will be available on a companion website.
This book bridges the gap between playing with robots in school and studying robotics at the upper undergraduate and graduate levels to prepare for careers in industry and research. Robotic algorithms are presented formally, but using only mathematics known by high-school and first-year college students, such as calculus, matrices and probability. Concepts and algorithms are explained through detailed diagrams and calculations.
Elements of Robotics presents an overview of different types of robots and the components used to build robots, but focuses on robotic algorithms: simple algorithms like odometry and feedback control, as well as algorithms for advanced topics like localization, mapping, image processing, machine learning and swarm robotics. These algorithms are demonstrated in simplified contexts that enable detailed computations to be performed and feasible activities to be posed. Students who study these simplified demonstrations will be well prepared for advanced study of robotics.
The algorithms are presented at a relatively abstract level, not tied to any specific robot. Instead a generic robot is defined that uses elements common to most educational robots: differential drive with two motors, proximity sensors and some method of displaying output to the user.The theory is supplemented with over 100 activities, most of which can be successfully implemented using inexpensive educational robots. Activities that require more computation can be programmed on a computer. Archives are available with suggested implementations for the Thymio robot and standalone programs in Python.