El Logic Theorist (LT) es un programa que demuestra teoremas de lógica proposicional. Lo escribieron Allen Newell, Herbert Simon y Cliff Shaw en la RAND Corporation entre 1955 y 1956, y suele presentarse como el primer programa de inteligencia artificial: una máquina que no calcula números sino que manipula símbolos para encontrar pruebas (Newell y Simon, 1956). Es el ejemplar tipo de lo que Haugeland (1985) bautizaría GOFAI, la IA simbólica «a la antigua».
Cómo funciona
El LT recibe los cinco axiomas proposicionales de los Principia Mathematica de Whitehead y Russell (*1.2 a *1.6), algunas definiciones y un teorema del capítulo 2 para probar. Tiene pocos métodos: sustitución (instanciar las variables de un axioma o teorema conocido hasta que coincida con la meta), desprendimiento (el modus ponens: si quiero B y tengo A → B, me basta probar A) y encadenamiento hacia adelante o hacia atrás. Por ejemplo, *2.01, (p → ¬p) → ¬p, sale de *1.2, (p ∨ p) → p, sustituyendo p por ¬p y reescribiendo ¬p ∨ ¬p como p → ¬p por definición.
Cada método que no cierra la prueba deja subproblemas en una lista, que el programa recorre hasta encontrar una prueba o agotar un límite de esfuerzo. Eso es búsqueda heurística: enumerar todas las secuencias de fórmulas hasta dar con una prueba es posible en principio y absurdo en la práctica; trabajar hacia atrás desde la meta poda ese espacio a costa de no garantizar nada. Cada teorema probado, además, pasa a la memoria y sirve de premisa para los siguientes.
Según Newell et al. (1957), el LT probó 38 de los primeros 52 teoremas del capítulo 2 y, para *2.85, encontró una prueba más corta que la de los Principia. Simon se la mostró a Russell, quien, según el relato de Simon, respondió encantado.
Dónde apareció
Newell y Simon llegaron al taller de Dartmouth del verano de 1956 con el programa ya especificado y simulado a mano (Shrager, 2026), algo que casi nadie más tenía. Mitchell cuenta que allí se reunieron los futuros «cuatro grandes» del campo, McCarthy, Minsky, Newell y Simon, y que salieron del encuentro con un optimismo enorme (M. Mitchell, 2019, ch. 1). El 11 de septiembre de ese año el LT abrió la segunda jornada del Simposio de Teoría de la Información del MIT; ese mismo día Noam Chomsky presentó «Three models for the description of language», y ambos trabajos salieron en el mismo número de las IRE Transactions on Information Theory. George Miller (2003) fecha en esa jornada la concepción de las ciencias cognitivas: la IA simbólica y la gramática generativa se presentaron en la misma sala.
Qué dejó
Para programar el LT, el equipo inventó IPL, un lenguaje de listas, símbolos y recursión que es antecesor directo de Lisp (Shrager, 2026). Sus heurísticas se generalizaron en el General Problem Solver, que resolvía acertijos como el de los misioneros y los caníbales (M. Mitchell, 2019, ch. 1), y luego se especializaron en los sistemas expertos, que cambiaron la búsqueda general por muchas reglas de dominio. La idea de buscar en un árbol con buenas heurísticas llega hasta Deep Blue y AlphaGo. Filosóficamente, el LT fue, en retrospectiva, una primera prueba de concepto de lo que Newell y Simon llamarían la hipótesis del sistema físico de símbolos (Newell y Simon, 1976).
Límites
El LT solo conoce un fragmento pequeño y decidible de la lógica, y sus heurísticas, escritas a mano, no aprenden. Mitchell señala un rasgo de toda la familia: si se reemplaza MISIONEROS por «Z372B», el programa funciona exactamente igual, porque para la máquina el significado de un símbolo se reduce a cómo se combina y se opera con él (M. Mitchell, 2019, ch. 1). Los modelos de razonamiento actuales invierten la receta: heurísticas aprendidas de los datos, pruebas que no siempre pueden auditarse paso a paso.