Mathematical Logic for Computer ScienceMathematical Logic for Computer Science is a mathematics textbook with theorems and proofs, but the choice of topics has been guided by the needs of computer science students. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound and yet sufficiently elementary for undergraduates. To provide a balanced treatment of logic, tableaux are related to deductive proof systems. The logical systems presented are: - Propositional calculus (including binary decision diagrams); - Predicate calculus; - Resolution; - Hoare logic; - Z; - Temporal logic. Answers to exercises (for instructors only) as well as Prolog source code for algorithms may be found via the Springer London web site: http: //www.springer.com/978-1-85233-319-5 Mordechai Ben-Ari is an associate professor in the Department of Science Teaching of the Weizmann Institute of Science. He is the author of numerous textbooks on concurrency, programming languages and logic, and has developed software tools for teaching concurrency. In 2004, Ben-Ari received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education. |
Contents
II | 1 |
III | 2 |
IV | 3 |
V | 5 |
VI | 6 |
VII | 7 |
VIII | 9 |
IX | 12 |
XLVII | 150 |
XLVIII | 152 |
XLIX | 153 |
L | 155 |
LI | 164 |
LII | 171 |
LIII | 173 |
LIV | 176 |
X | 17 |
XI | 19 |
XII | 24 |
XIII | 29 |
XIV | 33 |
XV | 38 |
XVI | 40 |
XVII | 43 |
XVIII | 45 |
XIX | 48 |
XX | 56 |
XXI | 59 |
XXII | 60 |
XXIII | 64 |
XXIV | 67 |
XXV | 81 |
XXVI | 88 |
XXVII | 95 |
XXVIII | 99 |
XXIX | 101 |
XXXI | 102 |
XXXII | 105 |
XXXIII | 107 |
XXXIV | 109 |
XXXV | 118 |
XXXVI | 120 |
XXXVII | 121 |
XXXVIII | 125 |
XXXIX | 127 |
XL | 129 |
XLI | 134 |
XLII | 135 |
XLIII | 138 |
XLIV | 139 |
XLV | 142 |
XLVI | 148 |
LV | 181 |
LVI | 186 |
LVII | 194 |
LVIII | 199 |
LIX | 201 |
LXI | 202 |
LXII | 209 |
LXIII | 211 |
LXIV | 213 |
LXV | 216 |
LXVI | 219 |
LXVII | 221 |
LXX | 224 |
LXXI | 235 |
LXXIII | 236 |
LXXIV | 239 |
LXXV | 242 |
LXXVI | 252 |
LXXVII | 255 |
LXXVIII | 257 |
LXXX | 262 |
LXXXI | 264 |
LXXXII | 266 |
LXXXIII | 272 |
LXXXIV | 280 |
LXXXV | 283 |
LXXXVI | 284 |
LXXXVII | 286 |
LXXXVIII | 287 |
LXXXIX | 288 |
XC | 289 |
XCI | 291 |
XCII | 293 |
297 | |
299 | |
Other editions - View all
Common terms and phrases
A₁ algorithm applied arbitrary assignment Assumption atomic formula axioms B₁ binary binary decision diagram Boolean operators branch C₁ C₂ called clashing clausal form closed computation construction decision procedure deductive system defined Definition denoted disjunction domain element equations equivalent Example extend_tableau failure node false finite function symbols Gentzen goal clause graph Herbrand Herbrand base Hintikka structure interpretation labeled leaf Lemma logic programming mathematical model checking MSCC negation notation OBDD Peterson's algorithm postcondition predicate calculus Prolog proof propositional calculus prove recursive refutation resolution resolvent rule s₁ satisfiable semantic tableau semantic tree sequence set of clauses set of formulas set of literals skolem specification ẞ-rule subformulas subset substitution temporal logic terminates Theorem true truth table truth values unifier universal quantifiers unsatisfiable valid variables VxA(x Vxq(x wp(S wp(W xp(x