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 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 non-classical logics, the translation method is detailed. Logic for Computer Science and Artificial Intelligence is the classroom-tested result of several years of teaching at Grenoble INP (Ensimag). It is conceived to allow self-instruction 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. 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 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 Non-classical Logics, The. 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. Ricardo Caferra. Includes Bibliographical References And Index. Cover 1 Logic for Computer Science and Artificial Intelligence 3 Title Page 5 Copyright Page 6 Table of Contents 7 Preface 13 Chapter 1. Introduction 15 1.1. Logic, foundations of computer science, and applications of logic to computer science 15 1.2. On the utility of logic for computer engineers 17 Chapter 2. A Few Thoughts Before the Formalization 21 2.1. What is logic? 21 2.1.1. Logic and paradoxes 22 2.1.2. Paradoxes and set theory 23 2.1.2.1. The answer 24 2.1.3. Paradoxes in arithmetic and set theory 27 2.1.3.1. The halting problem 27 2.1.4. On formalisms and well-known notions 29 2.1.4.1. Some “well-known” notions that could turn out to be difficult to analyze 33 2.1.5. Back to the definition of logic 37 2.1.5.1. Some definitions of logic for all 38 2.1.5.2. A few more technical definitions 38 2.1.5.3. Theory and meta-theory (language and meta-language) 44 2.1.6. A few thoughts about logic and computer science 44 2.2. Some historic landmarks 46 Chapter 3. Propositional Logic 53 3.1. Syntax and semantics 54 3.1.1. Language and meta-language 57 3.1.2. Transformation rules for cnf and dnf 63 3.2. The method of semantic tableaux 68 3.2.1. A slightly different formalism: signed tableaux 72 3.3. Formal systems 78 3.3.1. A capital notion: the notion of proof 78 3.3.2. What do we learn from the way we do mathematics? 86 3.4. A formal system for PL (PC) 92 3.4.1. Some properties of formal systems 98 3.4.2. Another formal system for PL (PC) 100 3.4.3. Another formal system 100 3.5. The method of Davis and Putnam 106 3.5.1. The Davis–Putnam method and the SAT problem 109 3.6. Semantic trees in PL 110 3.7. The resolution method in PL 115 3.8. Problems, strategies, and statements 123 3.8.1. Strategies 124 3.9. Horn clauses 127 3.10. Algebraic point of view of propositional logic 128 Chapter 4. First-order Terms 135 4.1. Matching and unification 135 4.1.1. A motivation for searching for a matching algorithm 135 4.1.2. A classification of trees 137 4.2. First-order terms, substitutions, unification 139 Chapter 5. First-Order Logic (FOL) or Predicate Logic (PL1, PC1) 145 5.1. Syntax 147 5.2. Semantics 151 5.2.1. The notions of truth and satisfaction 153 5.2.2. A variant: multi-sorted structures 164 5.2.2.1. Expressive power, sort reduction 164 5.2.3. Theories and their models 166 5.2.3.1. How can we reason in FOL? 167 5.3. Semantic tableaux in FOL 168 5.4. Unification in the method of semantic tableaux 180 5.5. Toward a semi-decision procedure for FOL 183 5.5.1. Prenex normal form 183 5.5.1.1. Skolemization 188 5.5.2. Skolem normal form 190 5.6. Semantic trees in FOL 200 5.6.1. Skolemization and clausal form 202 5.7. The resolution method in FOL 204 5.7.1. Variables must be renamed 215 5.8. A decidable class: the monadic class 216 5.8.1. Some decidable classes 219 5.9. Limits: Gödel’s (first) incompleteness theorem 220 Chapter 6. Foundations of Logic Programming 227 6.1. Specifications and programming 227 6.2. Toward a logic programming language 233 6.3. Logic programming: examples 236 6.3.1. Acting on the execution control: cut “/” 243 6.3.1.1. Translation of imperative structures 245 6.3.2. Negation as failure (NAF) 246 6.3.2.1. Some remarks about the strategy used by LP and negation as failure 252 6.3.2.2. Can we simply deduce instead of using NAF? 253 6.4. Computability and Horn clauses 255 Chapter 7. Artificial Intelligence 259 7.1. Intelligent systems: AI 259 7.2. What approaches to study AI? 263 7.3. Toward an operational definition of intelligence 263 7.3.1. The imitation game proposed by Turing 264 7.4. Can we identify human intelligence with mechanical intelligence? 265 7.4.1. Chinese room argument 266 7.5. Some history 268 7.5.1. Prehistory 268 7.5.2. History 269 7.6. Some undisputed themes in AI 270 Chapter 8. Inference 273 8.1. Deductive inference 274 8.2. An important concept: clause subsumption 280 8.2.1. An important problem 282 8.3. Abduction 287 8.3.1. Discovery of explanatory theories 288 8.3.1.1. Required conditions 289 8.4. Inductive inference 292 8.4.1. Deductive inference 293 8.4.2. Inductive inference 294 8.4.3. Hempel’s paradox (1945) 294 8.5. Generalization: the generation of inductive hypotheses 298 8.5.1. Generalization from examples and counter examples 302 Chapter 9. Problem Specification in Logical Languages 305 9.1. Equality 305 9.1.1. When is it used? 306 9.1.2. Some questions about equality 306 9.1.3. Why is equality needed? 307 9.1.4. What is equality? 307 9.1.5. How to reason with equality? 309 9.1.6. Specification without equality 310 9.1.7. Axiomatization of equality 311 9.1.8. Adding the definition of = and using the resolution method 311 9.1.9. By adding specialized rules to the method of semantic tableaux 313 9.1.10. By adding specialized rules to resolution 314 9.1.10.1. Paramodulation and demodulation 314 9.2. Constraints 323 9.3. Second Order Logic (SOL): a few notions 333 9.3.1. Syntax and semantics 338 9.3.1.1. Vocabulary 338 9.3.1.2. Syntax 339 9.3.1.3. Semantics 339 Chapter 10. Non-classical Logics 341 10.1. Many-valued logics 341 10.1.1. How to reason with p-valued logics? 348 10.1.1.1. Semantic tableaux for p-valued logics 348 10.2. Inaccurate concepts: fuzzy logic 351 10.2.1. Inference in FL 362 10.2.1.1. Syntax 363 10.2.1.2. Semantics 363 10.2.2. Herbrand’s method in FL 364 10.2.2.1. Resolution and FL 365 10.3. Modal logics 367 10.3.1. Toward a semantics 369 10.3.1.1. Syntax (language of modal logic) 371 10.3.1.2. Semantics 372 10.3.2. How to reason with modal logics? 374 10.3.2.1. Formal systems approach 374 10.3.2.2. Translation approach 375 10.4. Some elements of temporal logic 385 10.4.1. Temporal operators and semantics 388 10.4.1.1. A famous argument 389 10.4.2. A temporal logic 391 10.4.3. How to reason with temporal logics? 392 10.4.3.1. The method of semantic tableaux 393 10.4.4. An example of a PL for linear and discrete time: PTL (or PLTL) 395 10.4.4.1. Syntax 395 10.4.4.2. Semantics 396 10.4.4.3. Method of semantic tableaux for PLTL (direct method) 397 Chapter 11. Knowledge and Logic: Some Notions 399 11.1. What is knowledge? 400 11.2. Knowledge and modal logic 403 11.2.1. Toward a formalization 403 11.2.2. Syntax 403 11.2.2.1. What expressive power? An example 403 11.2.2.2. Semantics 403 11.2.3. New modal operators 405 11.2.3.1. Syntax (extension) 405 11.2.3.2. Semantics (extension) 405 11.2.4. Application examples 406 11.2.4.1. Modeling the muddy children puzzle 406 11.2.4.2. Corresponding Kripke worlds 406 11.2.4.3. Properties of the (formalization chosen for the) knowledge 408 Chapter 12. Solutions to the Exercises 409 Bibliography 529 Index 531 Logic for Computer Science and Artificial Intelligence is the classroom-tested result of several years of teaching at Grenoble INP (Ensimag). It is conceived to allow self instruction 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. Book jacket.