El Basilisco, número 2

 

José Antonio López Brugos

«Notas sobre la mecanización de las deducciones lógicas»

El Basilisco, número 2, mayo-junio 1978, páginas 83-92.

Desde Aristóteles hasta los intentos recientes de prueba automática de teoremas la historia de la lógica ha recorrido un camino en el que la construcción de diagramas y máquinas lógicas ha tenido papel, como ilustra, por ejemplo el libro de M. Gardner, Máquinas lógicas y diagramas (ed. Grijalbo, México 1973). Un hito en esta historia es la máquina de Jevons (1869) para probar teoremas de álgebra de Boole.
Recientemente, desde mediados de los años 50, los lógicos estaban empeñados en construir programas para la prueba de teoremas lógicos con computadoras en dos direcciones: una, de interés para psicólogos y pedagogos, básicamente a partir de métodos llamados heurísticos (inteligencia artificial), y otra con el interés más puramente lógico de investigar en la teoría de la deducción, utilizando métodos fundamentalmente algorítmicos (complementados frecuentemente con recursos heurísticos). La deducción formal automática se divide en dos familias de métodos: la deducción natural (tablas) y los procedimientos de Herbrand (resolución).
En esta nota me centraré en la historia de esas dos familias de métodos, sin tratar de describirlos técnicamente, y dejando para otra ocasión los programas.

Facsímil del original impreso de este artículo en formato pdf