Reseña

Es usual pensar que la programación es una actividad centrada en datos y control. Esto es verdad, pero solo parcialmente, pues la programación lógica es un paradigma de programación que nos obliga a pensar en esta actividad desde otro punto de vista, uno según el cual esta labor está centrada, más bien, en justificaciones e inferencias usando lógica clásica. Por esta razón, este paradigma está asociado a la demostración automática con lógica clásica también; pero como la lógica no está restringida a la lógica clásica —y tenemos otros sistemas como las lógicas terministas de impronta tradicional, aristotélica, silogística—, la demostración automática tampoco requiere de la lógica clásica. Con esto en mente, hemos desarrollado este libro como una introducción a la demostración automática tradicional —que no una introducción a la demostración automática, para lo que hay otros materiales. Una introducción, sin embargo, atípica por tres razones: primero, porque presentamos cinco sistemas de lógica tradicional allende la silogística asertórica con todo y sus métodos arborescentes; segundo, porque ofrecemos implementaciones de estos métodos arborescentes para ofrecer asistentes de demostración automática; y tercero, porque desarrollamos un concepto general de demostración automática basado en la lógica tradicional. Dicho de otro modo, el propósito de este libro es (re)introducir a la silogística en los marcos normativos de la demostración automática haciendo uso de lógicas de términos contemporáneas.