
Programas para deducción automatizada en lógica proposicional: 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...