Zhe Hou - Fundamentals of Logic and Computation: With Practical Automated Reasoning and Verification

More information about this series at https://link.springer.com/bookseries/3191

This Springer imprint is published by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

It is no coincidence that some universities, such as the University of Pennsylvania and the Australian National University, have a Logic and Computation research group, and many offer courses under the same name. The fields of logic and computation are intrinsically related to each other, although the connection has only been made explicit since 1980.

Despite that there are plenty of excellent courses and material about logic and computation around the world, most of them treat the two topics separately. My personal favourites are John Harrisons Handbook of Practical Logic and Automated Reasoning and Hopcroft, Motwani and Ullmans Introduction to Automata Theory, Languages, and Computation, both of which heavily inspire this book. It is also difficult to find a single course that delivers theories of the two topics with practical exercises in modern tools. This book aims to address the two problems by compressing and unifying important concepts of the two areas and providing exercises in widely-used software applications. We give a transition from logic to computation via linear temporal logic and state machines.

The first half of the course is accompanied by exercises in Isabelle/HOL, which is a popular and user-friendly theorem prover. The second half of the course involves modelling and verification in Process Analysis Toolkit (PAT), a feature-rich model checker based on Hoares Communicating Sequential Processes. This book also provides entry-level tutorials for Isabelle/HOL and PAT. The hybrid skill set of practical theorem proving and model checking should be helpful for the future of readers should they pursue a research career or engineering in formal methods.

This course has 21 hours of lectures and 20 hours of tutorials/labsevery section corresponds to 1 hour of lecture and 1 hour of lab. The final chapter serves as the conclusion of the book and has no exercises. Sections in Part II of this book are noticeably longer than those in Part I, so they may require more hours. In reality, the user can allocate 6 hours of lectures for each of Chaps. ), and many examples of PAT models built into the software, should the user decide to extend the hours of labs. I also recommend devising large group projects on formal verification tasks during the course.

The road map of this book is illustrated below.

This book is written for two sets of audiences. Undergraduate students who are getting a Bachelors degree in computer science should at least pass this course. Higher degree research (HDR) students who excel at this course should have the foundation to pursue a Ph.D. degree in computer science.

All men are mortal.

Socrates is a man.

Therefore, Socrates is mortal.

All X are Y.

a is an X.

Therefore, a is Y.