Propositional Logic: Deduction and AlgorithmsThis account of propositional logic concentrates on the algorithmic translation of important methods, especially of decision procedures for (subclasses of) propositional logic. Important classical results and a series of new results taken from the fields of normal forms, satisfiability and deduction methods are arranged in a uniform and complete theoretic framework. The algorithms presented can be applied to VLSI design, deductive databases and other areas. After introducing the subject the authors discuss satisfiability problems and satisfiability algorithms with complexity considerations, the resolution calculus with different refinements, and special features and procedures for Horn formulas. Then, a selection of further calculi and some results on the complexity of proof procedures are presented. The last chapter is devoted to quantified boolean formulas. The algorithmic approach will make this book attractive to computer scientists and graduate students in areas such as automated reasoning, logic programming, complexity theory and pure and applied logic. |
Contents
Preface | 5 |
1 | 5 |
Exercises | 13 |
4 | 42 |
1 | 50 |
2 | 56 |
4 | 79 |
5 | 95 |
3 | 142 |
4 | 200 |
3 | 217 |
8 | 279 |
Calculi | 293 |
3 | 311 |
Quantified Formulas | 339 |
| 385 | |
Common terms and phrases
A₁ algorithm applied atoms calculus cnf-formula Computer conjunctive normal form consider contains data structure Davis-Putnam Davis-Putnam algorithm define deleted denote DHORN empty clause equivalent formula example exists false foreach formula in CNF free variables Hilbert Horn clauses Horn formulas hyperresolution inconsistent formula initial formula input resolution k-CNF lemma length loop method minimal mulas multiple occurrences multisets N-resolution negation negation normal form negative clause negative literals normal form NP-complete number of atoms obtain parent clauses polynomial positive literals Prolog Prolog programs proof propositional formulas propositional logic Q-Res Q-unit quantified boolean formulas reduced refutationally complete representation resolution derivation resolution refutation resolution step resolvent restriction return(false return(true rule satisfiability equivalent satisfiability problem satisfying truth assignment sequent sequent calculus SLD-resolution strongly connected component subformula tableau Theorem transformation Unique-SAT unit resolution Unit-Res V-literals y₁