Logic in Computer Science (Q4830107)

[For a review of the first edition (2000) see Zbl 0955.68001.] This book provides an elegant introduction to formal reasoning that is relevant to computation science. This second edition improves the first one with extra and expanded sections on temporal logic model checking, SAT solvers, second-order logic, the Alloy specification language, and programming by contract. The material is up-to-date and practical and is organized as follows: Chapter 1 is devoted to natural deduction techniques and the design, correctness and complexity of a SAT solver for full propositional classical logic. Chapter 2 deals with several issues about predicate logic: undecidability, expressiveness, etc. Also, an object modelling language, Alloy, is defined. Alloy is an automatic (model based) property-verification approach. This tool finds models which form counterexamples to assertions made by the user. In Chapter 3, a full exposition of a verification method of model checking is introduced. Model checking is an important tool on the design and debugging of a system and it is based on temporal logic. In Chapter 4, verification methods for sequential programms running on a simple process are introduced. This chapter contains a new section on the contract-programming paradigm of verifying program correctness. Chapter 5 is devoted to a logic engineering approach by using modal logic. The main case study is the logic of knowledge in multiagent systems. Finally, Chapter 6 concerns Boolean functions, a descriptive formalism for many hardware and software systems such as asynchronous circuits and reactive systems.