Confieso que he leído
1 Lógica
1.1 Lógica básica
Figura 1: Mosterín: Lógica de primer orden.
Figura 2: Mosterín: Teoría axiomática de conjuntos.
1.2 Lógica elemental
Figura 3: Pabion: Logique mathématique.
Figura 4: Enderton: A mathematical introduction to logic.
Figura 5: Shoenfield: Mathematical logic
1.3 Teoría de modelos
Figura 6: Chang+Keisler. Model theory.
1.4 Teoría de conjuntos
Figura 7: Halmos: Naive set theory.
Figura 8: Enderton: Elements of set theory.
Figura 9: Jech: Set theory
Figura 10: Hrbacek y Jech: Introduction to set theory
Figura 11: Devlin: Fundamentals of contemporary set theory
1.5 Lógica algebraica
Figura 12: Barnes y Mack: Una introducción algebraica a la lógica matemática.
Figura 13: Goldblatt: Topoi: The categorial analysis of logic.
1.6 Teoría de la computabilidad
Figura 14: Hermes: Introducción a la teoría de la computabilidad.
Figura 15: Cutland: Computability: An introduction to recursive function theory
2 Programación
Figura 16: La revolución informática (1)
Figura 17: La revolución informática (2)
2.1 Lisp
Figura 18: Winston y Horn: Lisp
Figura 19: Wertz: Lisp (Introducción a la programación)
Figura 20: Norvig: Paradigms of artificial intelligence programming: Case studies in Common Lisp.
2.2 ML
Figura 21: Paulson: ML for the working programmer.
Figura 22: Huet: Formal structures for computation and deduction
2.3 Scheme
Figura 23: Abelson-Sussman: Structure and interpretation of computer programs
Figura 24: Springer y Friedman: Scheme and the art of programming.
2.4 Prolog
Figura 25: Clocksin y Mellish: Programming in Prolog
Figura 26: Bratko: Prolog programming for artificial intelligence.
Figura 27: Sterling y Shapiro: The art of Prolog (Advanced programming techniques).
Figura 28: Nilsson y Maluszynski: Logic, programming and Prolog
Figura 29: O'Keefe: The craft of Prolog
Figura 30: Covington, Nute y Vellino: Prolog programming in depth.
Figura 31: Boizumault: The implementation of Prolog.
2.5 CLIPS
Figura 32: Giarrantano y Riley: Expert systems principles and programming
Figura 33: Kowalski y Levy: Rule-based programming
2.6 Haskell
Figura 34: Bird: Introducción a la programación funcional con Haskell.
Figura 35: Doets y van Eijck: The Haskell road to logic, maths and programming.
Figura 36: Hutton: Programming in Haskell
Figura 37: Rabhi y Lapalme: Algorithms: A functional programming approach.
Figura 38: Bird: Pearls of functional algorithm design.
3 Inteligencia artificial
3.1 Aproximación a la IA
Figura 39: Polya: Cómo plantear y resolver problemas.
Figura 40: Kowalski: Lógica, programación e inteligencia artificial.
Figura 41: Delahaye: Outils logiques pour l’intelligence artificielle.
3.2 Fundamentos de la IA
Figura 42: Nilsson: Principles of artificial intelligence.
Figura 43: Winston: Inteligencia artificial
Figura 44: Rich y Knight: Inteligencia artificial.
Figura 45: Russell y Norvig: Inteligencia artificial (un enfoque moderno)
3.3 Lógica e IA
Figura 46: Genesereth y Nilsson: Logical foundations of artificial intelligence
Figura 47: Shoham: Artificial intelligence techniques in Prolog
Figura 48: Flach: Simply logical (Intelligent reasoning by example)
Figura 49: Poole, Mackworth y Goebel: Computational intelligence (A logical approach)
3.4 Representación del conocimiento y razonamiento
Figura 50: Brachman y Levesque: Knowledge representation and reasoning.
Figura 51: Baral: Knowledge representation, reasoning and declarative problem solving.
Figura 52: Gelfond y Kahl: Knowledge representation, reasoning, and the design of intelligent agents (The answer-set programming approach).
4 Lógica computacional
4.1 Demostración automática
Figura 53: Chang y Lee: Symbolic Logic and Mechanical Theorem Proving.
Figura 54: Loveland: Automated theorem proving (A logical basis).
Figura 55: Bundy: The computer modelling of mathematical reasoning
Figura 56: Winkler: The Church-Rosser property in computer algebra and special theorem proving: an investigation of critical-pair/completion algorithms
Figura 57: Baader y Nipkow: Term rewriting and all that.
Figura 58: Wu: Mechanical theorem proving in geometries: Basic principles.
Figura 59: Harrison: Handbook of practical logic and automated reasoning
4.2 Cálculo simbólico
Figura 60: Rayna: Reduce: Software for algebraic computation
4.3 Programación lógica
Figura 61: Lloyd: Foundations of logic programming
Figura 62: Maier y Warren: Computing with Logic (Logic Programming with Prolog)
Figura 63: Apt: From logic programming to Prolog
Figura 64: Doets: From logic to logic programming.
4.4 Lógica para la computación
Figura 65: Schöning: Logic for computer scientists.
Figura 66: Gallier: Logic for computer science: Foundations of automatic theorem proving.
Figura 67: Ben Ari: Mathematical logic for computer
Figura 68: Fitting: First-order logic and automated theorem proving
Figura 69: Huth y Ryan: Logic in computer science: Modelling and reasoning about systems.
4.5 Demostración asistida por ordenador
4.5.1 Otter
Figura 70: Wos: Automated reasoning (Introduction and applications).
Figura 71: Quaife: Automated development of fundamental mathematical theories
4.5.2 Nqthm
Figura 72: Boyer y Moore: A computational logic
Figura 73: Kunen: Non-constructive computational mathematics.
Figura 74: Shankar: Metamathematics, machines and Gödel's proof
4.5.3 ACL2
Figura 75: Kaufmann, Manolios y Moore: Computer-aided reasoning: An approach
4.5.4 PVS
Figura 76: Shankar: A tutorial introduction to PVS
4.5.5 Isabelle
Figura 77: Nipkow, Paulson y Wenzel: Isabelle/HOL (A proof assistant for higher-order logic).
4.5.6 Coq
Figura 78: Peirce: Software foundations Vol. 1: Logical foundations
Figura 79: Smolka: Computational type theory and interactive theorem proving with Coq.
4.5.7 Agda
Figura 80: Stump: Verified functional programming in Agda
4.5.8 Lean
Figura 81: Avigad: Theorem proving in Lean
Figura 82: Avigad: Logic and proof