Programas para deducción automatizada en lógica proposicional

Abstract

El proyecto de controlar el razonamiento y reducirlo a una segura operación de cálculo cuenta ya con siglos; pero no cabe duda de que el desarrollo de los ordenadores le ha dado nuevos impulsos. En la actualidad el objetivo del razonamiento automatizado es escribir programas de ordenador que nos ayuden en la solución de problemas en los que se requiera razonar. Nuestro objetivo al escribir los programas que aquí se ofrecen para deducción automatizada de teoremas en lógica preposicional ha sido múltiple: 1. Ofrecer al lector interesado pero no especialista unas técnicas no siempre de fácil acceso. 2. Desarrollar unos programas en los que se atienda especialmente a la estrategia seguida en la demostración de los teoremas. 3. Por su construcción centrada en las estrategias deductivas, crecemos que los programas pueden cumplir también una función tutorial, de ayuda en el aprendizaje de la lógica elemental. En I se dan las características y reglas de los cálculos que vamos a usar. En II se exponen las estrategias deductivas para cada uno. En III se comentan los programas. En IV se valora su rendimiento. En V se da una mínima bibliografía.