I bought this as a mathematical logic book, not so much for the computer science. I think the author's computer science perspective helps enormously with the clarification of mathematical logic for mathematicians.
Out of the 45 books which I have bought on mathematical logic, this one by Mordechai Ben-Ari stands out for its lucidity. Most of the books on mathematical logic for mathematicians are written from the perspective of deep research into various theoretical issues in model theory, ordinal number theory, completeness, relative consistency, axiom of choice, and so forth. For most applied and pure mathematics, these deep theory issues have no practical relevance, although the professional mathematician does need to understand them at least to some extent. Ben-Ari's intended applications in computer science seem to keep the logic in this book down to Earth, although the presentation has all of the integrity which is required by mathematicians for practical deduction and theoretical understanding.
My personal strong preference in logic is to use natural deduction, which was popularised by Gentzen in his 1934/35 papers in Mathematische Zeitschrift. This book by Ben-Ari also gives substantial coverage to Gentzen's full sequent calculus, not as a logic research tool, but as a practical deduction system. My only complaint about Gentzen's logic systems is the tableaux which are typically used to explain them. Ben-Ari does use tableaux a lot, but this actually enhances the presentation.
Side by side with the Gentzen systems, Ben-Ari also gives Hilbert systems, which require every proposition in a deduction to be true, whereas in Gentzen systems, every deduction line is a conditional proposition. It's unusual to see full presentations of both styles of logic closely side by side as is done here. This helps to clarify the relations between Gentzen and Hilbert systems.
One tiny complaint I have about this book is that the "abbreviation" SAT is nowhere defined. I spent a lot of time trying to find the meaning within this book and on the web. I eventually concluded that it is not an abbreviation for 3 words. It apparently means "SATisfiability" or "SATisfaction", or something like that. But I guess the computer science people would know all about that already!
3 people found this helpful.
Was this review helpful to you?
20JUN11 2ND EDITION+BOOK BY SCHONING On 20 June 2011, I received the 2nd edition of this book by Mordechai Ben-Ari Mathematical Logic for Computer Science, along with a shorter book on similar subjects by Uwe Schoning Logic for Computer Scientists (Modern Birkhäuser Classics). The Schoning book became my all time favorite, while the Ben-Ari 2nd Ed was heavily computational, including a lot of actual Prolog code in plaintext, and seemed rather clumsy to this non-computer scientist reader.
GENERAL COMMENTS / COMPARISON OF 3RD ED. AND 2ND ED. This new 2012 3rd edition is massively better organized than the 2nd, with for this reader also much better content as a computational logic book, or even as a general purpose logic book. Try both editions with the Amazon 'Look Inside' utility to see what is included in each of them. The new edition removed all the Prolog code to a website, and there is much more coverage of many aspects of propositional and first-order logics, including their resolution methods. Some coverage of interesting temporal logic is again included, as well as final chapters on program verification for both sequential and concurrent programs. One other thing improved in 3rd Ed is just terminology, calling the logics 'logic' instead of 'calculus'. With the previous edition's use of that old terminology, its title could logically have been 'Mathematical Calculi for Computer Science'.
A rather surprising thing for this type of book is that truth and falsity use the traditional T and F rather than the less ambiguous bits of 1 and 0. Schoning used 1 and 0, as did Joel Robbin in his great 1969 logic book Mathematical Logic: A First Course (Dover Books on Mathematics). So far, the Schoning and the Robbin are my favorite two logic texts for content, and I have read all of both of them. The present much longer book might yet have a shot at being preferable to those two books. We'll see. By chapter 4 of the present worthwhile book, it will not in any way unseat the primacy of the Schoning and the Robbin as my ultimate logic textbooks.
THE CHAPTERS AND THEIR STARTING PAGES Preface-vi / 1 Introduction-1 / 2 Propositional Logic: Formulas, Models, Tableaux-7 / 3 Propositional Logic: Deductive Systems-49 / 4 Propositional Logic: Resolution-75 / 5 Propositional Logic: Binary Decision Diagrams-95 / 6 Propositional Logic: SAT Solvers-111 / 7 First-Order Logic: Formulas, Models, Tableaux-131 / 8 First-Order Logic: Deductive Systems-155 / 9 First-Order Logic: Terms and Normal Forms-167 / 10 First-Order Logic: Resolution-185 / 11 First-Order Logic: Logic Programming-205 / 12 First-Order Logic: Undecidability and Model Theory*-223 / 13 Temporal Logic: Formulas, Models, Tableaux-231 / 14 Temporal Logic: A Deductive System-263 / 15 Verification of Sequential Programs-273 / 16 Verification of Concurrent Programs-297 / Appendix: Set Theory-327 / Index of Symbols-337 / Name Index-339 / Subject Index-341
READING THIS 3RD EDITION CHAPTERS 1 AND 2 Started reading this 3rd edition on Thu 27Sep12 afternoon. Short introductory chapter 1 is a good one for giving an overview of subjects in the book, plus a bit of motivation. Chapter 2, the first one of several on propositional logic gets right down to computational methods with pseudocode algorithms for logical parse trees and related ideas, plus some reverse polish context-free assembly code, all well done. There are also more than the usual propositional connectives ('operators' in this book), now including xor, nand, and nor, as well as the usual not, and, or, implication and the biconditional (or equivalence). It seems silly to me to carry around nand/not-and and nor/not-or as separate operators, although xor is distinct from the usual logical or. In section 2.4.2, it turns out that nand and nor have a defining property that no other operators have, so nand and nor are uniquely useful for that. Not silly then, but usage of the extra operators mostly ends in chapter 3 already, with only xor showing up a bit later.
Further into chapter 2, things start getting a bit more traditional, with even a few truth tables. The author spent a little time discussing normal vs. exclusive or, and double headed arrow vs. 3 horizontal bar equivalence. Quite interesting. This was followed by some good substitution issues and minimizing what operators (connectives) are needed, all well done. Very good semantic tableau tree proof methods get laid out on pages 33-39, and then soundness and completeness for propositional trees are discussed and proved on pages 39-44 as the last main subject in long chapter 2. Finished quite interesting chapter 2 and started chapter 3 on propositional deductive systems on Fri 5Oct12 afternoon. Here ends my detailed review of chapter reading in this book.
Briefly, chapter 3 on propositional deductive systems mostly covers well a Hilbert system of deduction, and it is a very good, moderately practical chapter. It ultimately does become a bit tedious though with its MANY rather clumsy Hilbert-style proofs. Sequent calculus mentioned late seems to be the best deductive method. Finished chap 3 Tue 9Oct12.
Chapter 4 is on propositional resolution, a standard method in computational logic, covered extremely well in Schoning chapter 1. The Ben-Ari chap 4 seems somewhat vague and wandering, but it is still worthwhile to read as another decent treatment of the subject. Don't recommend reading wandering * section 4.4 or especially difficult * section 4.5. Finished limited read of chap 4 Sat 13Oct12 afternoon.
Chapter 5 on Binary Decision Diagrams (BDDs) only to p. 100 in section 5.3 on Sun 14Oct12. In chap 5, the BDDs that were the subject were supposed to be directed graphs, but the author never put the arrow heads in to show them as digraphs. Decided to read some sections of chapter 6 on SAT solvers. Started that and chapter 7 both on Mon 15Oct12.
Chapter 6 on SAT solvers thru section 6.3. That gets thru listing the DPLL algorithm. 6.4 is a tedious long example I'd never understand. Then to quite interesting sections 6.5-6.9, finishing this chapter mid day Wed 17Oct12.
Chapter 7, the initial one on first-order logic starts out very well, with a good treatment. Finished chap 7 minus several proofs early pm on Mon 22Oct12.
Chapter 9 next on terms and normal forms. Most interesting chapter yet! It features a lot of theories by Skolem and by Herbrand. Finished Fri 26Oct12.
A nicely rather concrete version of resolution for first-order logic in chapter 10, finished except for last * section Mon 29Oct12.
Skipped chapter 11 because Schoning's much longer and super well written chapter 3 on logic programming was quite superior to Ben-Ari's short corresponding chapter.
Fully * chapter 12 is intensely interesting to this reader, but unfortunately it is only an 8 page very sketchy and incomplete chapter. My reading of this book ends with chapter 12 in afternoon of Tue 30Oct12.
34 days to read most of chapters 1-10 and chapter 12 in this book.
21 people found this helpful.
Was this review helpful to you?