Ricardo Caferra, LIG, CNRS/Grenoble INP, France.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.

• Preface xiChapter 1. Introduction 11.1. Logic, foundations of computer science, and applications of logic to computer science 11.2. On the utility of logic for computer engineers 3Chapter 2. A Few Thoughts Before the Formalization 72.1. What is logic? 72.2. Somehistoric landmarks 32Chapter 3. Propositional Logic 393.1. Syntaxand semantics 403.2. Themethodof semantic tableaux 543.3. Formal systems 643.4. Aformal systemforPL(PC) 783.5. ThemethodofDavis andPutnam 923.6. Semantic trees inPL 963.7. The resolutionmethodinPL 1013.8. Problems, strategies, andstatements 1093.9. Hornclauses 1133.10. Algebraic point of view of propositional logic 114Chapter 4. First-order Terms 1214.1. Matchingandunification 1214.2. First-order terms, substitutions, unification 125Chapter 5. First-Order Logic (FOL) or Predicate Logic (PL1, PC1) 1315.1. Syntax 1335.2. Semantics 1375.3. Semantic tableauxin FOL 1545.4. Unification in the method of semantic tableaux 1665.5. Toward a semi-decision procedure for FOL 1695.6. Semantic trees inFOL 1865.7. The resolutionmethodinFOL 1905.8. Adecidable class: themonadic class 2025.9. Limits: Godel’s (first) incompleteness theorem 206Chapter 6. Foundations of Logic Programming 2136.1. Specifications and programming 2136.2. Toward a logic programming language 2196.3. Logicprogramming: examples 2226.4. Computability and Horn clauses 241Chapter 7. Artificial Intelligence 2457.1. Intelligent systems: AI 2457.2. What approaches to studyAI? 2497.3. Toward an operational definition of intelligence 2497.4. Can we identify human intelligence with mechanicalintelligence? 2517.5. Somehistory 2547.6. Some undisputed themes in AI 256Chapter 8. Inference 2598.1. Deductiveinference 2608.2. An important concept: clause subsumption 2668.3. Abduction 2738.4. Inductive inference 2788.5. Generalization: the generation of inductive hypotheses 284Chapter 9. Problem Specification in Logical Languages 2919.1. Equality 2919.2. Constraints 3099.3. Second Order Logic (SOL): a few notions 319Chapter 10. Non-classical Logics 32710.1. Many-valuedlogics 32710.2. Inaccurate concepts: fuzzy logic 33710.3. Modal logics 35310.4. Some elements of temporal logic 371Chapter 11. Knowledge and Logic: Some Notions 38511.1. What is knowledge? 38611.2. Knowledge and modal logic 389Chapter 12. Solutions to the Exercises 395Bibliography 515Index 517