En informática , en particular en la representación y el razonamiento del conocimiento y la metalógica , el área del razonamiento automatizado se dedica a comprender diferentes aspectos del razonamiento . El estudio del razonamiento automatizado ayuda a producir programas informáticos que permiten a las computadoras razonar de forma completa, o casi completa, de forma automática. 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 automatizada de teoremas (y el subcampo menos automatizado pero más pragmático de la demostración interactiva de teoremas ) y la verificación de pruebas automatizada (vista como un razonamiento correcto garantizado bajo supuestos fijos). [ cita requerida ] También se ha realizado un trabajo extenso en el razonamiento por analogía utilizando la inducción y la 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 minimidad 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 un simple demostrador 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 máxima entropía y muchas técnicas ad hoc menos formales .
El desarrollo de la lógica formal jugó 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 se ha verificado hasta los axiomas fundamentales de las matemáticas. Se proporcionan 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. Por tanto, 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 de Teórico de la Lógica 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]