No label defined (Q4488342)

[For a review of the German original (Teubner, Stuttgart, 1994) see Zbl 0809.03003.] This book contains a treatment of propositional logic, both from a classical mathematical standpoint, as well as from a modern computer-oriented standpoint, e.g. treating data structures for the representation of formulas and clauses, implementation details for several calculi and deduction algorithms, as well as worst-case and average-case complexity estimations. In this respect, the topics treated in this book and the style of presentation, as well as the computer science viewpoint to logic, is quite unique and refreshing. The first chapter deals with notation and basic results. Then, in the second chapter, data structures for the representation of clauses and normal forms are discussed, including binary decision diagrams. The satisfiability problem of propositional logic (which is NP-complete) and various algorithms and deduction systems for solving it, like the Davis-Putnam algorithm, are discussed in detail in Chapter 3. A large part of Chapter 3 is devoted to the complexity of a variety of satisfiability problems, or problems derived from satisfiability problems. Most of them turn out to be NP-complete, but some are complete for other classes, like PSPACE or DP. Another aspect is the evolution of random satisfiability instances. Random formulas with few clauses tend to be satisfiable, then, starting at a certain threshold, random formulas with many clauses tend to be unsatisfiable. Resolution as a special system with a variety of computer science applications, its refinements and evaluation strategies are the themes of Chapter 4. The special case of Horn formulas together with deduction systems tailored for Horn logic is treated in the fifth chapter. Chapter 6 discusses all the other known calculi -- specialized to the case of propositional logic: Frege systems, cutting planes, tableau, segment calculus, and Gentzen systems. The relative strengths of these systems are compared. In Chapter 7, propositional formulas are equipped with quantifiers, but quantifiers that range only over Boolean values. These QBF formulas can be understood as some kind of intermediate step between propositional logic and predicate logic. Again, similar variations and algorithms as in the propositional case are presented for QBF.