Logic for computer science and artificial intelligence
 Responsibility
 Ricardo Caferra.
 Imprint
 London : ISTE ; Hoboken, NJ : Wiley, 2011.
 Physical description
 1 online resource (537 pages) : illustrations
Online
More options
Description
Creators/Contributors
 Author/Creator
 Caferra, Ricardo, 1945
Contents/Summary
 Bibliography
 Includes bibliographical references and index.
 Contents

 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 wellknown notions 15
 2.1.4.1 Some "wellknown" 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 metatheory (language and metalanguage) 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 metalanguage 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 DavisPutnam 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 Firstorder 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 Firstorder terms, substitutions, unification 125
 Chapter 5 FirstOrder 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: multisorted 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 semidecision 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 Nonclassical Logics 327
 l0.l Manyvalued logics 327
 10.1.1 How to reason with pvalued logics? 334
 10.1.1.1 Semantic tableaux for pvalued 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.
 Publisher's summary

Logic and its components (propositional, firstorder, nonclassical) 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 problematic and logic as a topic benefits from a unified approach. Logic for Computer Science and Artificial Intelligence utilizes this format, surveying the tableaux, resolution, Davis and Putnam methods, logic programming, as well as for example unification and subsumption. For nonclassical logics, the translation method is detailed. Logic for Computer Science and Artificial Intelligence is the classroomtested result of several years of teaching at Grenoble INP (Ensimag). It is conceived to allow selfinstruction for a beginner with basic knowledge in Mathematics and Computer Science, but is also highly suitable for use in traditional courses. The reader is guided by clearly motivated concepts, introductions, historical remarks, side notes concerning connections with other disciplines, and numerous exercises, complete with detailed solutions, The title provides the reader with the tools needed to arrive naturally at practical implementations of the concepts and techniques discussed, allowing for the design of algorithms to solve problems.
(source: Nielsen Book Data)
Subjects
Bibliographic information
 Publication date
 2011
 ISBN
 9781118604182 (electronic bk.)
 1118604180 (electronic bk.)
 9781118604205 (electronic bk.)
 1118604202 (electronic bk.)
 9781118604267
 1118604261
 1848213018
 9781848213012
 9781848213012