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...

Πλήρης περιγραφή

Λεπτομέρειες βιβλιογραφικής εγγραφής
Κύριος συγγραφέας: Caferra, Ricardo, 1945-
Μορφή: Ηλ. βιβλίο
Γλώσσα: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.