Abstract
En lo que sigue se ofrecerá un breve panorama de la manera en que se está realizando "el sueño de Leibniz", indicando algunas de sus propiedades y limitaciones. Pero más específicamente, se discutirá, en primer lugar, el papel que la deducción automática tiene en el desarrollo actual de la lógica matemática y, en segundo lugar, la importancia que tiene en la justificación filosófica de la inferencia deductiva. La investigación sobre la deducción automática aporta fundamentaciones "constructivas" de la lógica y un análisis de la inferencia lógica como un mecanismo para obtener conocimiento.