Logic for Computer Science and Artificial Intelligence

by Caferra, Ricardo

• ISBN13: 9781848213012
• ISBN10: 1848213018
• Edition: 1st
• Format: Hardcover
• Copyright: 2011-08-15
• Publisher: Wiley-ISTE

Summary

This book is the result of several years of teaching experience at Grenoble INP (Ensimag). It is essentially self-instruction oriented, but of course can be used in traditional courses. Logic (propositional, first-order, and non-classical) plays a key role in Computer Science and Artificial Intelligence. A huge amount of information exists in different supports (such as books, articles, and web pages), but to avoid becoming lost in these references, the beginner needs a unified, synthetic approach. Such an approach is followed throughout the book, which surveys tableaux, resolution, Davis and Putnam methods, and logic programming along with unification and subsumption. For non-classical logics, the translation method is privileged. Numerous historical remarks and digressions concerning connections with other domains, as well as a plethora of exercises including detailed solutions, will accompany the reader in his learning.

Author Biography

Ricardo Caferra has been involved in teaching and research in Computational Logic and Artificial intelligence for many years. He has published several works in both domains, particularly on some non-standard features of automated deduction.

Table of Contents

Preface	p. xi
Introduction	p. 1
Logic, foundations of computer science, and applications of logic to computer science	p. 1
On the utility of logic for computer engineers	p. 3
A Few Thoughts Before the Formalization	p. 7
What is logic?	p. 7
Logic and paradoxes	p. 8
Paradoxes and set theory	p. 9
The answer	p. 10
Paradoxes in arithmetic and set theory	p. 13
The halting problem	p. 13
On formalisms and well-known notions	p. 15
Some "well-known" notions that could turn out to be difficult to analyze	p. 19
Back to the definition of logic	p. 23
Some definitions of logic for all	p. 24
A few more technical definitions	p. 24
Theory and meta-theory (language and meta-language)	p. 30
A few thoughts about logic and computer science	p. 30
Some historic landmarks	p. 32
Propositional Logic	p. 39
Syntax and semantics	p. 40
Language and meta-language	p. 43
Transformation rules for cnf and dnf	p. 49
The method of semantic tableaux	p. 54
A slightly different formalism: signed tableaux	p. 58
Formal systems	p. 64
A capital notion: the notion of proof	p. 64
What do we learn from the way we do mathematics?	p. 72
A formal system for PL (PC)	p. 78
Some properties of formal systems	p. 84
Another formal system for PL (PC)	p. 86
Another formal system	p. 86
The method of Davis and Putnam	p. 92
The Davis-Putnam method and the SAT problem	p. 95
Semantic trees in PL	p. 96
The resolution method in PL	p. 101
Problems, strategies, and statements	p. 109
Strategies	p. 110
Horn clauses	p. 113
Algebraic point of view of propositional logic	p. 114
First-order Terms	p. 121
Matching and unification	p. 121
A motivation for searching for a matching algorithm	p. 121
A classification of trees	p. 123
First-order terms, substitutions, unification	p. 125
First-Order Logic (FOL) or Predicate Logic (PL1, PC1)	p. 131
Syntax	p. 133
Semantics	p. 137
The notions of truth and satisfaction	p. 139
A variant: multi-sorted structures	p. 150
Expressive power, sort reduction	p. 150
Theories and their models	p. 152
How can we reason in FOL?	p. 153
Semantic tableaux in FOL	p. 154
Unification in the method of semantic tableaux	p. 166
Toward a semi-decision procedure for FOL	p. 169
Prenex normal form	p. 169
Skolemization	p. 174
Skolem normal form	p. 176
Semantic trees in FOL	p. 186
Skolemization and clausal form	p. 188
The resolution method in FOL	p. 190
Variables must be renamed	p. 201
A decidable class: the monadic class	p. 202
Some decidable classes	p. 205
Limits: Gödel's (first) incompleteness theorem	p. 206
Foundations of Logic Programming	p. 213
Specifications and programming	p. 213
Toward a logic programming language	p. 219
Logic programming: examples	p. 222
Acting on the execution control: cut"/"	p. 229
Translation of imperative structures	p. 231
Negation as failure (NAF)	p. 232
Some remarks about the strategy used by LP and negation as failure	p. 238
Can we simply deduce instead of using NAF?	p. 239
Computability and Horn clauses	p. 241
Artificial Intelligence	p. 245
Intelligent systems: AI	p. 245
What approaches to study AI?	p. 249
Toward an operational definition of intelligence	p. 249
The imitation game proposed by Turing	p. 250
Can we identify human intelligence with mechanical intelligence?	p. 251
Chinese room argument	p. 252
Some history	p. 254
Prehistory	p. 254
History	p. 255
Some undisputed themes in AI	p. 256
Inference	p. 259
Deductive inference	p. 260
An important concept: clause subsumption	p. 266
An important problem	p. 268
Abduction	p. 273
Discovery of explanatory theories	p. 274
Required conditions	p. 275
Inductive inference	p. 278
Deductive inference	p. 279
Inductive inference	p. 280
Hempel's paradox (1945)	p. 280
Generalization: the generation of inductive hypotheses	p. 284
Generalization from examples and counter examples	p. 288
Problem Specification in Logical Languages	p. 291
Equality	p. 291
When is it used?	p. 292
Some questions about equality	p. 292
Why is equality needed?	p. 293
Whatis equality?	p. 293
How to reason with equality?	p. 295
Specification without equality	p. 296
Axiomatization of equality	p. 297
Adding the definition of = and using the resolution method	p. 297
By adding specialized rules to the method of semantic tableaux	p. 299
By adding specialized rules to resolution	p. 300
Paramodulation and demodulation	p. 300
Constraints	p. 309
Second Order Logic (SOL): a few notions	p. 319
Syntax and semantics	p. 324
Vocabulary	p. 324
Syntax	p. 325
Semantics	p. 325
Non-classical Logics	p. 327
Many-valued logics	p. 327
How to reason with p-valued logics?	p. 334
Semantic tableaux for p-valued logics	p. 334
Inaccurate concepts: fuzzy logic	p. 337
Inference in FL	p. 348
Syntax	p. 349
Semantics	p. 349
Herbrand's method in FL	p. 350
Resolution andFL	p. 351
Modal logics	p. 353
Toward a semantics	p. 355
Syntax (language of modal logic)	p. 357
Semantics	p. 358
How to reason with modallogics?	p. 360
Formal systems approach	p. 360
Translation approach	p. 361
Some elements of temporal logic	p. 371
Temporal operators and semantics	p. 374
A famous argument	p. 375
A temporal logic	p. 377
How to reason with temporal logics?	p. 378
The method of semantic tableaux	p. 379
An example of a PL for linear and discrete time; PTL (or PLTL)	p. 381
Syntax	p. 331
Semantics	p. 382
Method of semantic tableaux for PLTL (direct method)	p. 333
Knowledge and Logic: Some Notions	p. 385
What is knowledge?	p. 335
Knowledge and modal logic	p. 389
Toward a formalization	p. 389
Syntax	p. 339
What expressive power? An example	p. 389
Semantics	p. 339
New modal operators	p. 391
Syntax (extension)	p. 391
Semantics (extension)	p. 391
Application examples	p. 392
Modeling the muddy children puzzle	p. 392
Corresponding Kripke worlds	p. 392
Properties of the (formalization chosen for the) knowledge	p. 394
Solutions to the Exercises	p. 395
Bibliography	p. 515
Index	p. 517
Table of Contents provided by Ingram. All Rights Reserved.