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 proble...
| Otros Autores: | |
|---|---|
| Formato: | Libro electrónico |
| Idioma: | Inglés |
| Publicado: |
London, England ; Hoboken, New Jersey :
ISTE
2011.
|
| Edición: | 1st edition |
| Colección: | ISTE
|
| Materias: | |
| Ver en Biblioteca Universitat Ramon Llull: | https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009627739706719 |
Tabla de Contenidos:
- Cover; Logic for Computer Science and Artificial Intelligence; Title Page; Copyright Page; Table of Contents; Preface; Chapter 1. Introduction; 1.1. Logic, foundations of computer science, and applications of logic to computer science; 1.2. On the utility of logic for computer engineers; Chapter 2. A Few Thoughts Before the Formalization; 2.1. What is logic?; 2.1.1. Logic and paradoxes; 2.1.2. Paradoxes and set theory; 2.1.2.1. The answer; 2.1.3. Paradoxes in arithmetic and set theory; 2.1.3.1. The halting problem; 2.1.4. On formalisms and well-known notions
- 2.1.4.1. Some "well-known" notions that could turn out to be difficult to analyze2.1.5. Back to the definition of logic; 2.1.5.1. Some definitions of logic for all; 2.1.5.2. A few more technical definitions; 2.1.5.3. Theory and meta-theory (language and meta-language); 2.1.6. A few thoughts about logic and computer science; 2.2. Some historic landmarks; Chapter 3. Propositional Logic; 3.1. Syntax and semantics; 3.1.1. Language and meta-language; 3.1.2. Transformation rules for cnf and dnf; 3.2. The method of semantic tableaux; 3.2.1. A slightly different formalism: signed tableaux
- 3.3. Formal systems3.3.1. A capital notion: the notion of proof; 3.3.2. What do we learn from the way we do mathematics?; 3.4. A formal system for PL (PC); 3.4.1. Some properties of formal systems; 3.4.2. Another formal system for PL (PC); 3.4.3. Another formal system; 3.5. The method of Davis and Putnam; 3.5.1. The Davis-Putnam method and the SAT problem; 3.6. Semantic trees in PL; 3.7. The resolution method in PL; 3.8. Problems, strategies, and statements; 3.8.1. Strategies; 3.9. Horn clauses; 3.10. Algebraic point of view of propositional logic; Chapter 4. First-order Terms
- 4.1. Matching and unification4.1.1. A motivation for searching for a matching algorithm; 4.1.2. A classification of trees; 4.2. First-order terms, substitutions, unification; Chapter 5. First-Order Logic (FOL) or Predicate Logic (PL1, PC1); 5.1. Syntax; 5.2. Semantics; 5.2.1. The notions of truth and satisfaction; 5.2.2. A variant: multi-sorted structures; 5.2.2.1. Expressive power, sort reduction; 5.2.3. Theories and their models; 5.2.3.1. How can we reason in FOL?; 5.3. Semantic tableaux in FOL; 5.4. Unification in the method of semantic tableaux
- 5.5. Toward a semi-decision procedure for FOL5.5.1. Prenex normal form; 5.5.1.1. Skolemization; 5.5.2. Skolem normal form; 5.6. Semantic trees in FOL; 5.6.1. Skolemization and clausal form; 5.7. The resolution method in FOL; 5.7.1. Variables must be renamed; 5.8. A decidable class: the monadic class; 5.8.1. Some decidable classes; 5.9. Limits: Gödel's (first) incompleteness theorem; Chapter 6. Foundations of Logic Programming; 6.1. Specifications and programming; 6.2. Toward a logic programming language; 6.3. Logic programming: examples; 6.3.1. Acting on the execution control: cut "/"
- 6.3.1.1. Translation of imperative structures
