Hardcover
Published: 20th January 2004
ISBN: 9781852335656
Number Of Pages: 361
Earn 587 Qantas Points
on this Book
Logic and Complexity looks at basic logic as it is used in Computer Science, and provides students with a logical approach to Complexity theory. With plenty of exercises, this book presents classical notions of mathematical logic, such as decidability, completeness and incompleteness, as well as new ideas brought by complexity theory such as NP-completeness, randomness and approximations, providing a better understanding for efficient algorithmic solutions to problems.
Divided into three parts, it covers:
- Model Theory and Recursive Functions - introducing the basic model theory of propositional, 1st order, inductive definitions and 2nd order logic. Recursive functions, Turing computability and decidability are also examined.
- Descriptive Complexity - looking at the relationship between definitions of problems, queries, properties of programs and their computational complexity.
- Approximation - explaining how some optimization problems and counting problems can be approximated according to their logical form.
Logic is important in Computer Science, particularly for verification problems and database query languages such as SQL. Students and researchers in this field will find this book of great interest.
Introduction | p. 1 |
Basic model theory and computability | p. 3 |
Propositional logic | p. 5 |
Propositional language | p. 5 |
Construction of formulas | p. 5 |
Proof by induction | p. 7 |
Decomposition of a formula | p. 7 |
Semantics | p. 9 |
Tautologies. Equivalent formulas | p. 10 |
Logical consequence | p. 11 |
Value of a formula and substitution | p. 11 |
Complete systems of connectives | p. 15 |
Normal forms | p. 15 |
Disjunctive and conjunctive normal forms | p. 15 |
Functions associated to formulas | p. 16 |
Transformation methods | p. 17 |
Clausal form | p. 19 |
OBDD: Ordered Binary Decision Diagrams | p. 20 |
Exercises | p. 23 |
Deduction systems | p. 25 |
Examples of tableaux | p. 25 |
Tableaux method | p. 27 |
Trees | p. 28 |
Construction of tableaux | p. 29 |
Development and closure | p. 30 |
Completeness theorem | p. 31 |
Provable formulas | p. 31 |
Soundness | p. 31 |
Completeness | p. 32 |
Natural deduction | p. 33 |
Compactness theorem | p. 36 |
Exercices | p. 38 |
First-order logic | p. 41 |
First-order languages | p. 41 |
Construction of terms | p. 42 |
Construction of formulas | p. 43 |
Free and bound variables | p. 44 |
Semantics | p. 45 |
Structures and languages | p. 45 |
Structures and satisfaction of formulas | p. 46 |
Valid and equivalent formulas | p. 48 |
Substitution | p. 50 |
Prenex formulas and Skolem forms | p. 51 |
Prenex formulas and normal forms | p. 51 |
Skolem forms | p. 53 |
Exercises | p. 55 |
Completeness of first order logic | p. 57 |
Natural deduction sytem | p. 57 |
Soundness | p. 59 |
Completeness | p. 59 |
Examples of theories | p. 61 |
Successor function | p. 62 |
Discrete successor function | p. 62 |
Graphs | p. 63 |
Robinson's arithmetic | p. 64 |
Exercises | p. 65 |
Models of computation | p. 67 |
General model of computation | p. 67 |
Turing machines | p. 68 |
Deterministic Turing machines | p. 68 |
Non-deterministic Turing machines | p. 71 |
Machines with multiple tapes | p. 74 |
Turing machine with oracles | p. 76 |
Alternating machines | p. 76 |
Other sequential models of computation | p. 78 |
Finite automata | p. 78 |
RAM: Random Access Machines | p. 80 |
Exercises | p. 82 |
Recursion and decidability | p. 83 |
Recursive functions | p. 83 |
Primitive recursive functions | p. 83 |
Construction of primitive recursive functions | p. 84 |
Coding sequences | p. 86 |
Non-primitive recursion | p. 87 |
Recursive functions | p. 88 |
Church's thesis | p. 89 |
Recursion and computation | p. 90 |
Recursive functions are Turing computable | p. 90 |
Turing computable functions are recursive | p. 91 |
Universal Turing machine | p. 93 |
Recursive systems | p. 95 |
Equivalence with the recursive functions | p. 98 |
Implementation of recursive functions | p. 98 |
Recursion and decidability | p. 101 |
Recursive and recursively enumerable sets | p. 101 |
The halting problem | p. 103 |
Reductions | p. 104 |
The s-m-n and Rice's theorems | p. 105 |
Exercises | p. 107 |
Incompleteness of Peano arithmetic | p. 109 |
Arithmetic theory and representable functions | p. 109 |
Peano arithmetic | p. 109 |
Arithmetical proofs | p. 110 |
Non-standard models of arithmetic | p. 111 |
Representable functions | p. 111 |
Coding arithmetical proofs | p. 114 |
Coding terms and formulas | p. 115 |
Coding sequences of formulas | p. 116 |
Arithmetical theorems are recursively enumerable | p. 116 |
Undecidability and incompleteness | p. 117 |
The validity problem over finite structures | p. 118 |
The arithmetical hierarchy | p. 120 |
Exercises | p. 127 |
Descriptive Complexity | p. 129 |
Complexity: time and space | p. 131 |
Complexity classes | p. 132 |
Complexity of decision problems | p. 132 |
Examples of decision problems | p. 135 |
Complexity of search problems | p. 136 |
Hierarchies for time and space | p. 139 |
Simulation of several tapes | p. 139 |
The role of constants | p. 140 |
Relations between classes | p. 140 |
Hierarchies | p. 141 |
Non-deterministic space classes | p. 143 |
Other models and measures | p. 147 |
Random access machines | p. 147 |
Complexity on general structures | p. 148 |
Average and smoothed complexities | p. 148 |
Other measures | p. 148 |
Exercises | p. 150 |
First-order definability | p. 151 |
Explicit definitions | p. 151 |
Definability on a class of structures | p. 152 |
Partial elementary equivalence | p. 153 |
Ehrenfeucht-FraÃ¯ssÃ© games | p. 154 |
Logical characterization of r-equivalence | p. 156 |
Applications of Ehrenfeucht-FraÃ¯ssÃ© games | p. 158 |
Relational structures | p. 160 |
0-1 Law | p. 162 |
Loś-Vaught's test | p. 163 |
The theory of almost all relational structures | p. 163 |
Convergence and 0-1 law | p. 164 |
Implicit definitions | p. 166 |
Craig's interpolation theorem | p. 166 |
Beth's definability theorem | p. 168 |
Finite structures | p. 169 |
Exercises | p. 171 |
Inductive definitions and second-order logic | p. 175 |
Inductive definitions | p. 175 |
Inductive systems | p. 176 |
Fixed point logic | p. 178 |
Substitution | p. 179 |
Stage comparison | p. 180 |
Fixed point hierarchy | p. 182 |
Datalog | p. 184 |
Second-order logic | p. 186 |
Second-order formulas and interpretation | p. 186 |
Inductive definitions and second-order logic | p. 187 |
Exercises | p. 189 |
Time complexity : the classes P and NP | p. 191 |
The class NP and NP-complete problems | p. 191 |
Polynomial time reductions | p. 192 |
NP-complete problems | p. 192 |
Logical characterization of NP | p. 199 |
Examples of definable NP problems | p. 202 |
The logical characterizations of P and FP classes | p. 204 |
P: the class of global inductive relations | p. 204 |
FP: the class of global recursive functions | p. 208 |
Exercises | p. 211 |
Models of parallel computations | p. 213 |
The boolean circuits | p. 213 |
Complexity in parallel models | p. 217 |
Other circuits | p. 219 |
Examples of NC problems | p. 219 |
Matrix multiplication | p. 219 |
Csanky's matrix inversion algorithm | p. 220 |
The Parallel RAM | p. 223 |
Exercises | p. 226 |
Space complexity: the classes L, FL, NL and PSPACE | p. 229 |
The classes L, NL and FL | p. 230 |
NL-complete problems | p. 230 |
Alternation with space constraints | p. 231 |
Logical characterization of NL | p. 232 |
Logical characterization of FL | p. 236 |
Sequential space and parallel time | p. 241 |
The parallel time thesis | p. 243 |
P-complete problems | p. 243 |
The class PSPACE | p. 244 |
The quantified boolean formulas and the class AP | p. 244 |
Stochastic satisfiability | p. 246 |
Problems with uncertainty | p. 247 |
Exercises | p. 249 |
Definability of optimization and counting problems | p. 251 |
Optimization problems | p. 251 |
Counting problems | p. 257 |
The counting classes | p. 257 |
Definability of counting functions | p. 259 |
Exercises | p. 262 |
Approximation and classes beyond NP | p. 263 |
Probabilistic Classes | p. 265 |
Probabilistic decision classes | p. 265 |
Error amplification | p. 268 |
Comparing PP and #P | p. 269 |
Other probabilistic classes | p. 269 |
Examples of probabilistic algorithms | p. 270 |
Random walk in an undirected graph | p. 270 |
Perfect matching in a bipartite graph | p. 272 |
Solovay-Strassen primality test | p. 275 |
Exercises | p. 277 |
Probabilistic verification | p. 279 |
Interactive proofs | p. 280 |
Examples of interactive protocols | p. 281 |
The problem of non-isomorphism of graphs | p. 281 |
A protocol for the permanent | p. 283 |
A protocol for QBF | p. 285 |
Multiprover protocols | p. 289 |
Probabilistic checkable proofs PCP | p. 290 |
A PCP (n^{3}, 1) for 3SAT | p. 293 |
Exercises | p. 297 |
Approximation | p. 299 |
Optimization problems | p. 299 |
Examples of approximation algorithms | p. 301 |
Approximation of optimization problems | p. 304 |
Reductions and completeness | p. 309 |
Non-approximability | p. 311 |
Counting problems | p. 314 |
Approximation of counting problems | p. 314 |
Approximation of #DNF | p. 315 |
Approximate verification | p. 317 |
Exercises | p. 320 |
Classes beyond | p. 323 |
The polynomial hierarchy | p. 323 |
Second-order definability | p. 323 |
Relative computability | p. 324 |
Alternating machines | p. 326 |
Generalizations of NP | p. 327 |
The classes <$>oplus<$> P, PP and BPP | p. 328 |
Universal hashing | p. 331 |
The Valiant-Vazirani theorem | p. 333 |
Toda's theorem | p. 334 |
Exponential time | p. 338 |
Exercises | p. 342 |
Bibliography | p. 343 |
List of Figures | p. 349 |
Index | p. 353 |
Table of Contents provided by Publisher. All Rights Reserved. |
ISBN: 9781852335656
ISBN-10: 1852335653
Series: Discrete Mathematics and Theoretical Computer Science
Audience:
General
Format:
Hardcover
Language:
English
Number Of Pages: 361
Published: 20th January 2004
Publisher: SPRINGER VERLAG GMBH
Country of Publication: GB
Dimensions (cm): 23.39 x 15.6
x 2.24
Weight (kg): 0.7
Earn 587 Qantas Points
on this Book