Hispanopedia Wiki
Articulo de referencia

Razonamiento automatizado

En informática , en particular en la representación y razonamiento del conocimiento y la metalógica , el área del razonamiento automático se dedica a comprender diferentes aspec...

Hispanopedia WikiContenido en espanolLectura gratuita

En informática , en particular en la representación y razonamiento del conocimiento y la metalógica , el área del razonamiento automático se dedica a comprender diferentes aspectos del razonamiento . El estudio del razonamiento automático ayuda a producir programas informáticos que permiten a las computadoras razonar de forma completamente, o casi completamente, automática. Aunque el razonamiento automático 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 (vista como un razonamiento correcto garantizado bajo supuestos fijos). [ cita requerida ] También se ha realizado un trabajo extenso en 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 la argumentación, donde se aplican restricciones adicionales de minimalidad y consistencia además de la deducción automática más estándar. El sistema OSCAR de John Pollock [2] es un ejemplo de un sistema de argumentación automática que es más específico que un simple demostrador automático de teoremas.

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 .

Primeros años

El desarrollo de la lógica formal desempeñó un papel importante en el campo del razonamiento automático, 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 comprobado hasta los axiomas fundamentales de las matemáticas. Se proporcionan todos los pasos lógicos intermedios, sin excepción. No se hace ninguna apelación a la intuición, incluso si la traducción de la intuición a la lógica es rutinaria. Por lo 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 y científicos informáticos, como el origen del razonamiento automatizado, o deducción automatizada . [4] Otros dicen que comenzó antes de eso 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 automático, aunque es un área de investigación importante y popular, atravesó un " invierno de la IA " en los años ochenta y principios de los noventa. Sin embargo, el campo resurgió posteriormente. Por ejemplo, en 2005, Microsoft comenzó a utilizar tecnología de verificación en muchos de sus proyectos internos y está planeando incluir un lenguaje de verificación y especificación lógica en su versión 2012 de Visual C. [4]

Contribuciones significativas

Principia Mathematica fue una obra fundamental en la lógica formal escrita por Alfred North Whitehead y Bertrand Russell . Principia Mathematica (que también significa Principios de las matemáticas ) se escribió 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 y ocho de ellos. [7] Además de demostrar los teoremas, el programa encontró una prueba 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 :

"En el mundo existen hoy máquinas que piensan, que aprenden y que crean. Además, su capacidad para hacer estas cosas va a aumentar rápidamente hasta que (en un futuro visible) la gama de problemas que puedan resolver será tan extensa como la gama a la que se ha aplicado la mente humana." [8]

Ejemplos de pruebas formales

Sistemas de prueba

Demostrador del teorema de Boyer-Moore (NQTHM)
El diseño de NQTHM estuvo influenciado por John McCarthy y Woody Bledsoe. Se inició en 1971 en Edimburgo, Escocia, y era un demostrador de teoremas totalmente automático creado con Pure Lisp . Los aspectos principales de NQTHM fueron:
  1. el uso de Lisp como lógica de trabajo.
  2. la confianza en un principio de definición para funciones recursivas totales.
  3. el uso extensivo de la reescritura y la "evaluación simbólica".
  4. una heurística de inducción basada en el fracaso de la evaluación simbólica. [13] [14]
Luz HOL
HOL Light está escrito en OCaml y está diseñado para tener una base lógica simple y clara y una implementación despejada. Es esencialmente otro asistente de pruebas para la lógica clásica de orden superior. [15]
Gallo
Coq , desarrollado en Francia, es otro asistente de pruebas automatizado que puede extraer automáticamente programas ejecutables a partir de especificaciones, ya sea como código fuente Objective CAML o Haskell . Las propiedades, los programas y las pruebas se formalizan en el mismo lenguaje llamado Cálculo de construcciones inductivas (CIC). [16]

Aplicaciones

El razonamiento automatizado se ha utilizado con mayor frecuencia para construir demostradores de teoremas automatizados. Sin embargo, a menudo, los demostradores de teoremas requieren cierta guía humana para ser efectivos y, por lo tanto, se los califica más generalmente como asistentes de prueba . En algunos casos, estos demostradores han ideado nuevos enfoques para demostrar un teorema. Logic Theorist es un buen ejemplo de esto. El programa presentó una prueba para uno de los teoremas de Principia Mathematica que era más eficiente (requería menos pasos) que la prueba 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 tales problemas que se actualiza de forma regular. También existe una competencia entre demostradores de teoremas automatizados que se lleva a cabo regularmente en la conferencia CADE (Pelletier, Sutcliffe y Suttner 2002); Los problemas para la competición se seleccionan de la biblioteca TPTP. [17]

Véase también

Conferencias y talleres

Revistas

Comunidades

Referencias

  1. ^ Defourneaux, Gilles y Nicolas Peltier. "Analogía y abducción en la deducción automática". IJCAI (1). 1997.
  2. ^ John L. Pollock [ cita completa necesaria ]
  3. ^ C. Hales, Thomas "Formal Proof", Universidad de Pittsburgh. Recuperado el 19 de octubre de 2010.
  4. ^ ab "Deducción automática (AD)", [Proyecto La naturaleza de PRL] . Consultado el 19 de octubre de 2010
  5. ^ Martin Davis (1983). "La prehistoria y la historia temprana de la deducción automatizada". En Jörg Siekmann; G. Wrightson (eds.). Automatización del razonamiento (1) — Artículos clásicos sobre lógica computacional 1957–1966. Heidelberg: Springer. págs. 1–28. ISBN 978-3-642-81954-4.Aquí: p.15
  6. ^ "Principia Mathematica", en la Universidad de Stanford . Consultado el 19 de octubre de 2010.
  7. ^ "El teórico de la lógica y sus hijos". Consultado el 18 de octubre de 2010.
  8. ^ Shankar, Natarajan Little Engines of Proof , Laboratorio de Ciencias de la Computación, SRI International . Consultado el 19 de octubre de 2010.
  9. ^ Shankar, N. (1994), Metamatemáticas, máquinas y la prueba de Gödel, Cambridge, Reino Unido: Cambridge University Press, ISBN 9780521585330
  10. ^ Russinoff, David M. (1992), "Una prueba mecánica de reciprocidad cuadrática", J. Autom. Reason. , 8 (1): 3–21, doi :10.1007/BF00263446, S2CID  14824949
  11. ^ Gonthier, G.; et al. (2013), "Una prueba controlada por máquina del teorema de orden impar" (PDF) , en Blazy, S. ; Paulin-Mohring, C.; Pichardie, D. (eds.), Demostración interactiva de teoremas , Lecture Notes in Computer Science, vol. 7998, págs. 163–179, CiteSeerX 10.1.1.651.7964 , doi :10.1007/978-3-642-39634-2_14, ISBN  978-3-642-39633-5, S2CID  1855636
  12. ^ Heule, Marijn JH ; Kullmann, Oliver; Marek, Victor W. (2016). "Resolución y verificación del problema de las ternas pitagóricas booleanas mediante el método Cube-and-Conquer". Teoría y aplicaciones de las pruebas de satisfacibilidad – SAT 2016 . Apuntes de clase en informática. Vol. 9710. págs. 228–245. arXiv : 1605.00723 . doi :10.1007/978-3-319-40970-2_15. ISBN 978-3-319-40969-6.S2CID 7912943  .
  13. ^ El demostrador del teorema de Boyer-Moore Recuperado el 23 de octubre de 2010
  14. ^ Boyer, Robert S. y Moore, J Strother y Passmore, Grant Olney Archivo PLTP . Consultado el 27 de julio de 2023.
  15. ^ Harrison, John HOL Light: una visión general . Consultado el 23 de octubre de 2010.
  16. ^ Introducción a Coq . Consultado el 23 de octubre de 2010.
  17. ^ Razonamiento automatizado , Stanford Encyclopedia . Consultado el 10 de octubre de 2010.
  • Taller Internacional sobre Implementación de Lógicas
  • Serie de talleres sobre temas empíricamente exitosos en razonamiento automatizado
Obtenido de "https://es.wikipedia.org/w/index.php?title=Razonamiento_automatizado&oldid=1244179166"