The book provides a self-contained introduction to mathematical logic and computability theory for students of mathematics or computer science. It is organized around the failures and successes of Hilbert's programme for the formalization of Mathematics. It is widely known that the programme failed with Gödel's incompleteness theorems and related negative results about arithmetic. Unfortunately, the positive outcomes of the programme are less well known, even among mathematicians. The book covers key successes, like Gödel's proof of the completeness of first-order logic, Gentzen's proof of its consistency by purely symbolic means, and the decidability of a couple of useful theories. The book also tries to convey the message that Hilbert's programme made a significant contribution to the advent of the computer as it is nowadays understood and, thus, to the latest industrial revolution. Part I of the book addresses Hilbert's programme and computability. Part II presents first-order logic, including Gödel's completeness theorem and Gentzen's consistency theorem. Part III is focused on arithmetic, representability of computable maps, Gödel's incompleteness theorems and decidability of Presburger arithmetic. Part IV provides detailed answers to selected exercises. The book can be used at late undergraduate level or early graduate level. An undergraduate course would concentrate on Parts I and II, leaving out the Gentzen calculus, and sketching the way to the 1st incompleteness theorem. A more advanced course might skip early material already known to the students and concentrate on the positive and negative results of Hilbert's programme, thus covering Gentzen's proof of consistency and Part III in full.

This textbook aims to help the reader develop an in-depth understanding of logical reasoning and gain knowledge of the theory of computation. The book combines theoretical teaching and practical exercises; the latter is realised in Isabelle/HOL, a modern theorem prover, and PAT, an industry-scale model checker. I also give entry-level tutorials on the two software to help the reader get started. By the end of the book, the reader should be proficient in both software. Content-wise, this book focuses on the syntax, semantics and proof theory of various logics; automata theory, formal languages, computability and complexity. The final chapter closes the gap with a discussion on the insight that links logic with computation. This book is written for a high-level undergraduate course or a Master's course. 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.

In Memory of Dieter Rötting. 24.8.1937 - 4.6.1984. On the Occasion of the 50th Anniversary of His Birth

This must-read text presents the pioneering work of the late Professor Jacob (Jack) T. Schwartz on computational logic and set theory and its application to proof verification techniques, culminating in the ÆtnaNova system, a prototype computer program designed to verify the correctness of mathematical proofs presented in the language of set theory. Topics and features: describes in depth how a specific first-order theory can be exploited to model and carry out reasoning in branches of computer science and mathematics; presents an unique system for automated proof verification in large-scale software systems; integrates important proof-engineering issues, reflecting the goals of large-scale verifiers; includes an appendix showing formalized proofs of ordinals, of various properties of the transitive closure operation, of finite and transfinite induction principles, and of Zorn’s lemma.

ACM Monograph Series: A Computational Logic focuses on the use of induction in proving theorems, including the use of lemmas and axioms, free variables, equalities, and generalization. The publication first elaborates on a sketch of the theory and two simple examples, a precise definition of the theory, and correctness of a tautology-checker. Topics include mechanical proofs, informal development, formal specification of the problem, well-founded relations, natural numbers, and literal atoms. The book then examines the use of type information to simplify formulas, use of axioms and lemmas as rewrite rules, and the use of definitions. Topics include nonrecursive functions, computing values, free variables in hypothesis, infinite backwards chaining, infinite looping, computing type sets, and type prescriptions. The manuscript takes a look at rewriting terms and simplifying clauses, eliminating destructors and irrelevance, using equalities, and generalization. Concerns include reasons for eliminating isolated hypotheses, precise statement of the generalization heuristic, restricting generalizations, precise use of equalities, and multiple destructors and infinite looping. The publication is a vital source of data for researchers interested in computational logic.

A textbook on the semantics, proof theory, and metatheory of first-order logic. It covers naive set theory, first-order logic, sequent calculus and natural deduction, the completeness, compactness, and Löwenheim-Skolem theorems, Turing machines, and the undecidability of the halting problem and of first-order logic. It is based on the Open Logic project, and available for free download at slc.openlogicproject.org.

Although it is critical in today’s world that students who take automata theory and logic courses retain what they have learned and understand how to use their knowledge, many textbooks typically emphasize automata theory only, not logic, thus losing a valuable opportunity to tie these subjects together and reinforce learning. This textbook uses interactive tools throughout, such as simple BDD and SAT tools. By providing a blend of theory and practical applications the material is presented as both inviting and current. Key concepts are illustrated in multiple domains so that information is reinforced and students can begin to tie theory and logic together.