En informática , en particular en representación del conocimiento y razonamiento y 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 automatizada de pruebas (considerada como un razonamiento correcto garantizado bajo supuestos fijos). [ cita necesaria ] También se ha realizado un extenso trabajo en el razonamiento por analogía utilizando la inducción y la abducción . [1]
Otros temas importantes incluyen el razonamiento en condiciones de incertidumbre y el razonamiento no monótono . Una parte importante del campo de la incertidumbre es la de la argumentación, donde se aplican restricciones adicionales de minimalidad y coherencia 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 del 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 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 comparado con 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 Logic Theorist 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]
El razonamiento automatizado, aunque es un área de investigación importante y popular, pasó por un " invierno de la IA " en los años ochenta y principios de los noventa. Sin embargo, el campo revivió posteriormente. Por ejemplo, en 2005, Microsoft comenzó a utilizar tecnología de verificación en muchos de sus proyectos internos y planea incluir una especificación lógica y un lenguaje de verificación en su versión 2012 de Visual C. [4]
Principia Mathematica fue un trabajo histórico en lógica formal escrito por Alfred North Whitehead y Bertrand Russell . Principia Mathematica (que también significa Principios de Matemáticas ) fue escrita con el propósito de derivar todas o algunas de las expresiones matemáticas , en términos de lógica simbólica . Principia Mathematica se publicó inicialmente en tres volúmenes en 1910, 1912 y 1913. [6]
Logic Theorist (LT) fue el primer programa desarrollado en 1956 por Allen Newell , Cliff Shaw y Herbert A. Simon para "imitar el razonamiento humano" al demostrar teoremas y se demostró en cincuenta y dos teoremas del capítulo dos de Principia Mathematica, demostrando treinta -ocho de ellos. [7] Además de demostrar los teoremas, el programa encontró una demostración para uno de los teoremas que era más elegante que la proporcionada por Whitehead y Russell. Después de un intento fallido de publicar sus resultados, Newell, Shaw y Herbert informaron en su publicación de 1958, The Next Advance in Operation Research :
Ejemplos de pruebas formales
El razonamiento automatizado se ha utilizado con mayor frecuencia para crear demostradores de teoremas automatizados. Sin embargo, a menudo los demostradores de teoremas requieren cierta guía humana para ser efectivos y, por lo tanto, generalmente califican como asistentes de demostración . En algunos casos, estos demostradores han ideado nuevos enfoques para demostrar un teorema. El teórico de la lógica es un buen ejemplo de esto. El programa produjo una demostración de uno de los teoremas de Principia Mathematica que era más eficiente (requería menos pasos) que la demostración proporcionada por Whitehead y Russell. Los programas de razonamiento automatizado se están aplicando para resolver un número creciente de problemas en lógica formal, matemáticas e informática, programación lógica , verificación de software y hardware, diseño de circuitos y muchos otros. El TPTP (Sutcliffe y Suttner 1998) es una biblioteca de este tipo de problemas que se actualiza periódicamente. También hay una competencia entre demostradores automatizados de teoremas que se lleva a cabo periódicamente en la conferencia CADE (Pelletier, Sutcliffe y Suttner 2002); Los problemas para la competencia se seleccionan de la biblioteca TPTP. [17]