En informática , en particular en representación y razonamiento del conocimiento y metalógica , el área de razonamiento automatizado se dedica a comprender diferentes aspectos del razonamiento . El estudio del razonamiento automatizado ayuda a producir programas de computadora que permiten a las computadoras razonar completamente, o casi completamente, automáticamente. Aunque el razonamiento automatizado se considera un subcampo de la inteligencia artificial , también tiene conexiones con la informática teórica y la filosofía .
Las subáreas más desarrolladas del razonamiento automatizado son la demostración automática de teoremas (y el subcampo menos automatizado pero más pragmático de la demostración interactiva de teoremas ) y la verificación automática de pruebas (vista como un razonamiento correcto garantizado bajo suposiciones fijas). [ cita requerida ] También se ha realizado un extenso trabajo en el razonamiento por analogía usando inducción y abducción . [1]
Otros temas importantes incluyen el razonamiento bajo incertidumbre y el razonamiento no monótono . Una parte importante del campo de la incertidumbre es el de la argumentación, donde se aplican restricciones adicionales de minimalidad y consistencia además de la deducción automatizada más estándar. El sistema OSCAR de John Pollock [2] es un ejemplo de un sistema de argumentación automatizado que es más específico que ser solo un probador de teoremas automatizado.
Las herramientas y técnicas de razonamiento automatizado incluyen la lógica y los cálculos clásicos, la lógica difusa , la inferencia bayesiana , el razonamiento con entropía máxima y muchas técnicas ad hoc menos formales .
El desarrollo de la lógica formal desempeñó un papel importante en el campo del razonamiento automatizado, que a su vez condujo al desarrollo de la inteligencia artificial . Una prueba formal es una prueba en la que cada inferencia lógica ha sido comprobada hasta los axiomas fundamentales de las matemáticas. Se suministran todos los pasos lógicos intermedios, sin excepción. No se apela a la intuición, incluso si la traducción de la intuición a la lógica es rutinaria. Así, una prueba formal es menos intuitiva y menos susceptible a errores lógicos. [3]
Algunos consideran la reunión de verano de Cornell de 1957, que reunió a muchos lógicos e informáticos, como el origen del razonamiento automatizado, o deducción automatizada . [4] Otros dicen que comenzó antes con el programa Teórico Lógico de 1955 de Newell, Shaw y Simon, o con la implementación de Martin Davis en 1954 del procedimiento de decisión de Presburger (que demostró que la suma de dos números pares es par). [5]