Logic for computer science and artificial intelligence

Content: Chapter 1 Introduction 1 --
1.1 Logic, foundations of computer science, and applications of logic to computer science 1 --
1.2 On the utility of logic for computer engineers 3 --
Chapter 2 A Few Thoughts Before the Formalization 7 --
2.1 What is logic? 7 --
2.1.1 Logic and paradoxes 8 --
2.1.2 Paradoxes and set theory 9 --
l2.1.2.1 The answer 10 --
2.1.3 Paradoxes in arithmetic and set theory 13 --
2.1.3.1 The halting problem 13 --
2.1.4 On formalisms and well-known notions 15 --
2.1.4.1 Some \"well-known\" notions that could turn out to be difficult to analyze 19 --
2.1.5 Back to the definition of logic 23 --
2.1.5.1 Some definitions of logic for all 24 --
2.1.5.2 A few more technical definitions 24 --
2.1.5.3 Theory and meta-theory (language and meta-language) 30 --
2.1.6 A few thoughts about logic and computer science 30 --
2.2 Some historic landmarks 32 --
Chapter 3 Propositional Logic 39 --
3.1 Syntax and semantics 40 --
3.1.1 Language and meta-language 43 --
3.1.2 Transformation rules for cnf and dnf 49 --
3.2 The method of semantic tableaux 54 --
13.2.1 A slightly different formalism: signed tableaux 58 --
3.3 Formal systems 64 --
3.3.1 A capital notion: the notion of proof 64 --
3.3.2 What do we learn from the way we do mathematics? 72 --
3.4 A formal system for PL (PC) 78 --
3.4.1 Some properties of formal systems 84 --
3.4.2 Another formal system for PL (PC) 86 --
3.4.3 Another formal system 86 --
3.5 The method of Davis and Putnam 92 --
3.5.1 The Davis-Putnam method and the SAT problem 95 --
3.6 Semantic trees in PL 96 --
3.7 The resolution method in PL 101 --
3.8 Problems, strategies, and statements 109 --
3.8.1 Strategies 110 --
3.9 Horn clauses 113 --
3.10 Algebraic point of view of propositional logic 114 --
Chapter 4 First-order Terms 121 --
4.1 Matching and unification 121 --
4.1.1 A motivation for searching for a matching algorithm 121 --
4.1.2 A classification of trees 123 --
4.2 First-order terms, substitutions, unification 125 --
Chapter 5 First-Order Logic (FOL) or Predicate Logic (PL1, PC1) 131 --
5.1 Syntax 133 --
5.2 Semantics 137 --
5.2.1 The notions of truth and satisfaction 139 --
5.2.2 A variant: multi-sorted structures 150 --
5.2.2.1 Expressive power, sort reduction 150 --
5.2.3 Theories and their models 152 --
5.2.3.1 How can we reason in FOL? 153 --
5.3 Semantic tableaux in FOL 154 --
5.4 Unification in the method of semantic tableaux 166 --
5.5 Toward a semi-decision procedure for FOL 169 --
5.5.1 Prenex normal form 169 --
5.5.1.1 Skolemization 174 --
5.5.2 Skolem normal form 176 --
5.6 Semantic trees in FOL 186 --
5.6.1 Skolemization and clausal form 188 --
5.7 The resolution method in FOL 190 --
5.7.1 Variables must be renamed 201 --
5.8 A decidable class: the monadic class 202 --
5.8.1 Some decidable classes 205 --
5.9 Limits: Gödel\'s (first) incompleteness theorem 206 --
Chapter 6 Foundations of Logic Programming 213 --
6.1 Specifications and programming 213 --
6.2 Toward a logic programming language 219 --
6.3 Logic programming: examples 222 --
6.3.1 Acting on the execution control: cut\"/\" 229 --
6.3.1.1 Translation of imperative structures 231 --
6.3.2 Negation as failure (NAF) 232 --
6.3.2.1 Some remarks about the strategy used by LP and negation as failure 238 --
6.3.2.2 Can we simply deduce instead of using NAF? 239 --
6.4 Computability and Horn clauses 241 --
Chapter 7 Artificial Intelligence 245 --
7.1 Intelligent systems: AI 245 --
7.2 What approaches to study AI? 249 --
7.3 Toward an operational definition of intelligence 249 --
7.3.1 The imitation game proposed by Turing 250 --
7.4 Can we identify human intelligence with mechanical intelligence? 251 --
7.4.1 Chinese room argument 252 --
7.5 Some history 254 --
7.5.1 Prehistory 254 --
7.5.2 History 255 --
7.6 Some undisputed themes in AI 256 --
Chapter 8 Inference 259 --
8.1 Deductive inference 260 --
8.2 An important concept: clause subsumption 266 --
8.2.1 An important problem 268 --
8.3 Abduction 273 --
8.3.1 Discovery of explanatory theories 274 --
8.3.1.1 Required conditions 275 --
8.4 Inductive inference 278 --
8.4.1 Deductive inference 279 --
8.4.2 Inductive inference 280 --
8.4.3 Hempel\'s paradox (1945) 280 --
8.5 Generalization: the generation of inductive hypotheses 284 --
8.5.1 Generalization from examples and counter examples 288 --
Chapter 9 Problem Specification in Logical Languages 291 --
9.1 Equality 291 --
9.1.1 When is it used? 292 --
9.1.2 Some questions about equality 292 --
9.1.3 Why is equality needed? 293 --
9.1.4 Whatis equality? 293 --
9.1.5 How to reason with equality? 295 --
9.1.6 Specification without equality 296 --
9.1.7 Axiomatization of equality 297 --
9.1.8 Adding the definition of = and using the resolution method 297 --
9.1.9 By adding specialized rules to the method of semantic tableaux 299 --
9.1.10 By adding specialized rules to resolution 300 --
9.1.10.1 Paramodulation and demodulation 300 --
9.2 Constraints 309 --
9.3 Second Order Logic (SOL): a few notions 319 --
9.3.1 Syntax and semantics 324 --
9.3.1.1 Vocabulary 324 --
9.3.1.2 Syntax 325 --
9.3.1.3 Semantics 325 --
Chapter 10 Non-classical Logics 327 --
l0.l Many-valued logics 327 --
10.1.1 How to reason with p-valued logics? 334 --
10.1.1.1 Semantic tableaux for p-valued logics 334 --
10.2 Inaccurate concepts: fuzzy logic 337 --
10.2.1 Inference in FL 348 --
10.2.1.1 Syntax 349 --
10.2.1.2 Semantics 349 --
10.2.2 Herbrand\'s method in FL 350 --
10.2.2.1 Resolution andFL 351 --
10.3 Modal logics 353 --
10.3.1 Toward a semantics 355 --
10.3.1.1 Syntax (language of modal logic) 357 --
10.3.1.2 Semantics 358 --
10.3.2 How to reason with modallogics? 360 --
10.3.2.1 Formal systems approach 360 --
10.3.2.2 Translation approach 361 --
10.4 Some elements of temporal logic 371 --
10.4.1 Temporal operators and semantics 374 --
10.4.1.1 A famous argument 375 --
10.4.2 A temporal logic 377 --
10.4.3 How to reason with temporal logics? 378 --
10.4.3.1 The method of semantic tableaux 379 --
10.4.4 An example of a PL for linear and discrete time
 PTL (or PLTL) 381 --
10.4.4.1 Syntax 331 --
10.4.4.2 Semantics 382 --
10.4.4.3 Method of semantic tableaux for PLTL (direct method) 333 --
Chapter 11 Knowledge and Logic: Some Notions 385 --
11.1 What is knowledge? 335 --
11.2 Knowledge and modal logic 389 --
11.2.1 Toward a formalization 389 --
11.2.2 Syntax 339 --
11.2.2.1 What expressive power? An example 389 --
11.2.2.2 Semantics 339 --
11.2.3 New modal operators 391 --
11.2.3.1 Syntax (extension) 391 --
11.2.3.2 Semantics (extension) 391 --
11.2.4 Application examples 392 --
11.2.4.1 Modeling the muddy children puzzle 392 --
11.2.4.2 Corresponding Kripke worlds 392 --
11.2.4.3 Properties of the (formalization chosen for the) knowledge 394 --
Chapter 12 Solutions to the Exercises 395.