Logic for computer science and artificial intelligence /
Logic and its components (propositional, first-order, non-classical) play a key role in Computer Science and Artificial Intelligence. While a large amount of information exists scattered throughout various media (books, journal articles, webpages, etc.), the diffuse nature of these sources is proble...
Κύριος συγγραφέας: | |
---|---|
Μορφή: | Ηλ. βιβλίο |
Γλώσσα: | English |
Έκδοση: |
London :
ISTE ;
2011.
Hoboken, NJ : Wiley, 2011. |
Θέματα: | |
Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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.