| Autor(es) | J. Alan Robinson (1930–2016); Robert Kowalski (n. 1941); Alain Colmerauer (1941–2017); Philippe Roussel |
| Fecha / periodo | 1965–1974 · Siglo XX · Estados Unidos, Reino Unido y Francia |
| Tipo | Formal |
| Deriva de | Lógica de primer orden clásica |
| Derivan de ella | Lógicas no monótonas · Argumentación abstracta |
| Tres leyes | Identidad: ✓ (unificación: todo término unifica consigo mismo) · No contradicción: ✓ (la prueba es refutación: derivar la cláusula vacía de un conjunto contradictorio) · Tercio excluso: matizado (vale en la resolución clásica; con negación por fallo un átomo puede quedar indefinido) |
La resolución nació como un método para que las máquinas demostraran teoremas de primer orden. Los procedimientos anteriores, basados en el teorema de Herbrand, generaban instancias básicas a ciegas y se ahogaban en combinaciones. Robinson sustituyó todas las reglas del cálculo por una sola, la resolución, que opera sobre cláusulas y usa la unificación para elegir la instancia justa en el momento justo. Unos años después, Kowalski y Colmerauer advirtieron que, restringida a cláusulas de Horn, la búsqueda de una refutación se comporta como la ejecución de un programa: una cláusula «\(A\) si \(B_1\) y … y \(B_n\)» se lee a la vez como enunciado y como procedimiento. El gesto distintivo es la ecuación de Kowalski, «algoritmo = lógica + control»: el programador escribe lógica y el intérprete aporta la estrategia de búsqueda.
Forma clausal. Toda fórmula de primer orden se transforma, mediante forma prenexa, skolemización y forma normal conjuntiva, en un conjunto de cláusulas (disyunciones de literales con variables implícitamente universales) que es satisfacible si y solo si la fórmula lo es.
Unificación. Un unificador de dos expresiones es una sustitución que las hace idénticas. Robinson probó que si existe alguno, existe un unificador más general (mgu), único salvo renombramiento, y dio un algoritmo para calcularlo.
Regla de resolución (Robinson, «A machine-oriented logic based on the resolution principle», Journal of the ACM, 1965). De \(C \lor L\) y \(D \lor \neg L'\), si \(\sigma\) es el mgu de \(L\) y \(L'\), se infiere \((C \lor D)\sigma\). Se completa con la factorización, que unifica literales repetidos de una cláusula.
Teorema de completitud refutacional. Un conjunto de cláusulas es insatisfacible si y solo si la resolución deriva de él la cláusula vacía \(\square\). Para probar \(\Gamma \vdash \varphi\) se refuta \(\Gamma \cup \{\neg\varphi\}\). El procedimiento es semidecidible, como la propia lógica de primer orden.
Cláusulas de Horn. Cláusulas con a lo sumo un literal positivo:
Resolución SLD (Kowalski y Kuehner 1971; Kowalski 1974). Se selecciona un átomo del objetivo, se unifica con la cabeza de una cláusula del programa y se reemplaza por su cuerpo. Una derivación que llega al objetivo vacío produce una respuesta: la composición de las sustituciones. SLD es correcta y completa para programas de Horn (Clark, Hill). Prolog fija una estrategia concreta, izquierda a derecha y en profundidad con retroceso, que es incompleta: puede no terminar.
Semántica declarativa (van Emden y Kowalski, 1976). Para un programa de Horn \(P\), el menor modelo de Herbrand \(M_P\) coincide con el menor punto fijo del operador de consecuencia inmediata \(T_P\) y con el conjunto de átomos básicos derivables por SLD. Semántica de modelos, de puntos fijos y operacional coinciden.
Negación.
Ejemplo trabajado. Programa: \(\mathrm{padre}(ana, bea)\); \(\mathrm{padre}(bea, carla)\); \(\mathrm{antepasado}(X, Y) \leftarrow \mathrm{padre}(X, Y)\); \(\mathrm{antepasado}(X, Y) \leftarrow \mathrm{padre}(X, Z), \mathrm{antepasado}(Z, Y)\). Objetivo: \(\leftarrow \mathrm{antepasado}(ana, W)\). Primera respuesta: \(W = bea\). Por la segunda regla, con \(Z = bea\), el subobjetivo \(\mathrm{antepasado}(bea, W)\) da \(W = carla\). La refutación es a la vez la demostración y el cálculo.
Qué se pierde y qué se gana. Con la negación por fallo la consecuencia deja de ser monótona: añadir un hecho puede anular una conclusión negativa. El programa \(p \leftarrow \mathit{not}\ p\) no tiene modelo estable, y en la semántica bien fundada \(p\) queda indefinido.
La resolución procede de la lógica de primer orden clásica y, dentro de ella, de su metateoría: la forma normal de Skolem, el teorema de Herbrand (1930) y los procedimientos de prueba de Gilmore y de Davis y Putnam (1960). Robinson conservó el objetivo, que era un método completo de refutación para la lógica clásica, y cambió la técnica. La lectura procedimental de las cláusulas de Horn se forjó entre Edimburgo (Kowalski) y Marsella (Colmerauer y Roussel, que construyeron Prolog en 1972 a partir de un proyecto de procesamiento del lenguaje natural).
La relación con la lógica constructiva con negación fuerte es posterior: la negación fuerte de los programas lógicos extendidos (1991) se analizó mediante la lógica de Nelson en la lógica de equilibrio de Pearce, que dio una base lógica a la programación con conjuntos de respuestas. De la programación lógica derivan dos líneas. La hipótesis del mundo cerrado y la negación por fallo son precursoras directas de la lógica por defecto de Reiter y del resto de lógicas no monótonas. Las semánticas de modelos estables y bien fundados reaparecen, abstraídas, en la argumentación abstracta de Dung.
La programación lógica fue uno de los grandes programas de la inteligencia artificial simbólica. Japón la eligió como base de su proyecto de ordenadores de quinta generación (1982–1992), y Prolog se usó en sistemas expertos, procesamiento del lenguaje y bases de datos deductivas (Datalog). Hoy sobreviven Datalog, la programación con restricciones y la programación con conjuntos de respuestas, muy usada en planificación y combinatoria. Para la pregunta «¿una lógica o muchas?» el caso es doble. Por un lado, la resolución es un método para la lógica clásica. Por otro, la exigencia de ejecutar la lógica produjo una negación que no es la clásica, y la búsqueda de su semántica llevó a lógicas no monótonas, trivalentes e intermedias. Las necesidades del cálculo generaron lógicas nuevas.