Logic for Computer Science and Artificial Intelligence

Logic for Computer Science and Artificial Intelligence

by Ricardo Caferra
Released August 2011
Publisher(s): Wiley
ISBN: 9781118604267

Explore a preview version of Logic for Computer Science and Artificial Intelligence right now.

O’Reilly members get unlimited access to live online training experiences, plus books, videos, and digital content from 200+ publishers.

Start your free trial

Book Description

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.

Table of Contents

  1. Cover
  2. Title Page
  3. Copyright
  4. Preface
  5. Chapter 1: Introduction
    1. 1.1. Logic, foundations of computer science, and applications of logic to computer science
    2. 1.2. On the utility of logic for computer engineers
  6. Chapter 2: A Few Thoughts Before the Formalization
    1. 2.1. What is logic?
      1. 2.1.1. Logic and paradoxes
      2. 2.1.2. Paradoxes and set theory
        1. 2.1.2.1. The answer
      3. 2.1.3. Paradoxes in arithmetic and set theory
        1. 2.1.3.1. The halting problem
      4. 2.1.4. On formalisms and well-known notions
        1. 2.1.4.1. Some “well-known” notions that could turn out to be difficult to analyze
      5. 2.1.5. Back to the definition of logic
        1. 2.1.5.1. Some definitions of logic for all
        2. 2.1.5.2. A few more technical definitions
        3. 2.1.5.3. Theory and meta-theory (language and meta-language)
      6. 2.1.6. A few thoughts about logic and computer science
    2. 2.2. Some historic landmarks
  7. Chapter 3: Propositional Logic
    1. 3.1. Syntax and semantics
      1. 3.1.1. Language and meta-language
      2. 3.1.2. Transformation rules for cnf and dnf
    2. 3.2. The method of semantic tableaux
      1. 3.2.1. A slightly different formalism: signed tableaux
    3. 3.3. Formal systems
      1. 3.3.1. A capital notion: the notion of proof
      2. 3.3.2. What do we learn from the way we do mathematics?
    4. 3.4. A formal system for PL (PC)
      1. 3.4.1. Some properties of formal systems
      2. 3.4.2. Another formal system for PL (PC)
      3. 3.4.3. Another formal system
    5. 3.5. The method of Davis and Putnam
      1. 3.5.1. The Davis-Putnam method and the SAT problem
    6. 3.6. Semantic trees in PL
    7. 3.7. The resolution method in PL
    8. 3.8. Problems, strategies, and statements
      1. 3.8.1. Strategies
    9. 3.9. Horn clauses
    10. 3.10. Algebraic point of view of propositional logic
  8. Chapter 4: First-order Terms
    1. 4.1. Matching and unification
      1. 4.1.1. A motivation for searching for a matching algorithm
      2. 4.1.2. A classification of trees
    2. 4.2. First-order terms, substitutions, unification
  9. Chapter 5: First-Order Logic (FOL) or Predicate Logic (PL1, PC1)
    1. 5.1. Syntax
    2. 5.2. Semantics
      1. 5.2.1. The notions of truth and satisfaction
      2. 5.2.2. A variant: multi-sorted structures
        1. 5.2.2.1. Expressive power, sort reduction
      3. 5.2.3. Theories and their models
        1. 5.2.3.1. How can we reason in FOL?
    3. 5.3. Semantic tableaux in FOL
    4. 5.4. Unification in the method of semantic tableaux
    5. 5.5. Toward a semi-decision procedure for FOL
      1. 5.5.1. Prenex normal form
        1. 5.5.1.1. Skolemization
      2. 5.5.2. Skolem normal form
    6. 5.6. Semantic trees in FOL
      1. 5.6.1. Skolemization and clausal form
    7. 5.7. The resolution method in FOL
      1. 5.7.1. Variables must be renamed
    8. 5.8. A decidable class: the monadic class
      1. 5.8.1. Some decidable classes
    9. 5.9. Limits: Gödel’s (first) incompleteness theorem
  10. Chapter 6: Foundations of Logic Programming
    1. 6.1. Specifications and programming
    2. 6.2. Toward a logic programming language
    3. 6.3. Logic programming: examples
      1. 6.3.1. Acting on the execution control: cut “/”
      2. 6.3.2. Negation as failure (NAF)
        1. 6.3.2.1. Some remarks about the strategy used by LP and negation as failure
        2. 6.3.2.2. Can we simply deduce instead of using NAF?
    4. 6.4. Computability and Horn clauses
  11. Chapter 7: Artificial Intelligence
    1. 7.1. Intelligent systems: AI
    2. 7.2. What approaches to study AI?
    3. 7.3. Toward an operational definition of intelligence
      1. 7.3.1. The imitation game proposed by Turing
    4. 7.4. Can we identify human intelligence with mechanical intelligence?
      1. 7.4.1. Chinese room argument
    5. 7.5. Some history
      1. 7.5.1. Prehistory
      2. 7.5.2. History
    6. 7.6. Some undisputed themes in AI
  12. Chapter 8: Inference
    1. 8.1. Deductive inference
    2. 8.2. An important concept: clause subsumption
      1. 8.2.1. An important problem
    3. 8.3. Abduction
      1. 8.3.1. Discovery of explanatory theories
        1. 8.3.1.1. Required conditions
    4. 8.4. Inductive inference
      1. 8.4.1. Deductive inference
      2. 8.4.2. Inductive inference
      3. 8.4.3. Hempel’s paradox (1945)
    5. 8.5. Generalization: the generation of inductive hypotheses
      1. 8.5.1. Generalization from examples and counter examples
  13. Chapter 9: Problem Specification in Logical Languages
    1. 9.1. Equality
      1. 9.1.1. When is it used?
      2. 9.1.2. Some questions about equality
      3. 9.1.3. Why is equality needed?
      4. 9.1.4. What is equality?
      5. 9.1.5. How to reason with equality?
      6. 9.1.6. Specification without equality
      7. 9.1.7. Axiomatization of equality
      8. 9.1.8. Adding the definition of = and using the resolution method
      9. 9.1.9. By adding specialized rules to the method of semantic tableaux
      10. 9.1.10. By adding specialized rules to resolution
        1. 9.1.10.1. Paramodulation and demodulation
    2. 9.2. Constraints
    3. 9.3. Second Order Logic (SOL): a few notions
      1. 9.3.1. Syntax and semantics
        1. 9.3.1.1. Vocabulary
        2. 9.3.1.2. Syntax
        3. 9.3.1.3. Semantics
  14. Chapter 10: Non-Classical Logics
    1. 10.1. Many-valued logics
      1. 10.1.1. How to reason with p-valued logics?
        1. 10.1.1.1. Semantic tableaux for p-valued logics
    2. 10.2. Inaccurate concepts: fuzzy logic
      1. 10.2.1. Inference in FL
        1. 10.2.1.1. Syntax
        2. 10.2.1.2. Semantics
      2. 10.2.2. Herbrand’s method in FL
        1. 10.2.2.1. Resolution and FL
    3. 10.3. Modal logics
      1. 10.3.1. Toward a semantics
        1. 10.3.1.1. Syntax (language of modal logic)
        2. 10.3.1.2. Semantics
      2. 10.3.2. How to reason with modal logics?
        1. 10.3.2.1. Formal systems approach
        2. 10.3.2.2. Translation approach
    4. 10.4. Some elements of temporal logic
      1. 10.4.1. Temporal operators and semantics
        1. 10.4.1.1. A famous argument
      2. 10.4.2. A temporal logic
      3. 10.4.3. How to reason with temporal logics?
        1. 10.4.3.1. The method of semantic tableaux
      4. 10.4.4. An example of a PL for linear and discrete time: PTL (or PLTL)
        1. 10.4.4.1. Syntax
        2. 10.4.4.2. Semantics
        3. 10.4.4.3. Method of semantic tableaux for PLTL (direct method)
  15. Chapter 11: Knowledge and Logic: Some Notions
    1. 11.1. What is knowledge?
    2. 11.2. Knowledge and modal logic
      1. 11.2.1. Toward a formalization
      2. 11.2.2. Syntax
        1. 11.2.2.1. What expressive power? An example
        2. 11.2.2.2. Semantics
      3. 11.2.3. New modal operators
        1. 11.2.3.1. Syntax (extension)
        2. 11.2.3.2. Semantics (extension)
      4. 11.2.4. Application examples
        1. 11.2.4.1. Modeling the muddy children puzzle
        2. 11.2.4.2. Corresponding Kripke worlds
        3. 11.2.4.3. Properties of the (formalization chosen for the) knowledge
  16. Chapter 12: Solutions to the Exercises
  17. Bibliography
  18. Index

Product Information

  • Title: Logic for Computer Science and Artificial Intelligence
  • Author(s): Ricardo Caferra
  • Release date: August 2011
  • Publisher(s): Wiley
  • ISBN: 9781118604267