Diferencia entre revisiones de «A short survey of automated reasoning»
| (No se muestran 3 ediciones intermedias del mismo usuario) | |||
| Línea 1: | Línea 1: | ||
J. Harrison [http://www.cl.cam.ac.uk/~jrh13/papers/ab.html A short survey of automated reasoning]. ''Proceedings of the Second International Conference on Algebraic Biology, AB 2007''. Springer LNCS vol. 4545, pp. 334-349, 2007. | J. Harrison [http://www.cl.cam.ac.uk/~jrh13/papers/ab.html A short survey of automated reasoning]. ''Proceedings of the Second International Conference on Algebraic Biology, AB 2007''. Springer LNCS vol. 4545, pp. 334-349, 2007. | ||
---- | ---- | ||
| + | |||
El contenido del trabajo se resumen en: | El contenido del trabajo se resumen en: | ||
# Una breves historia de la automatización del razonamiento, | # Una breves historia de la automatización del razonamiento, | ||
| Línea 14: | Línea 15: | ||
Como ideas más interesantes destaco las siguientes: | Como ideas más interesantes destaco las siguientes: | ||
# La combinación de sistemas de cálculo simbólicos y demostradores de teoremas usando los primeros como "oráculos". | # La combinación de sistemas de cálculo simbólicos y demostradores de teoremas usando los primeros como "oráculos". | ||
| − | # La posibilidad de verificar los traductores de problemas combinatorios a SAT. | + | # La posibilidad de verificar los traductores de problemas combinatorios a SAT. A partir de esta idea se creó el proyecto [[Verificación de traductores de problemas combinatorios en SAT]]. |
| + | |||
| + | [[User:Jalonso|José A. Alonso]] 10:38, 12 November 2008 (CET) | ||
| + | |||
| + | [[Category:Lecturas]] | ||
Revisión actual del 11:38 12 nov 2008
J. Harrison A short survey of automated reasoning. Proceedings of the Second International Conference on Algebraic Biology, AB 2007. Springer LNCS vol. 4545, pp. 334-349, 2007.
El contenido del trabajo se resumen en:
- Una breves historia de la automatización del razonamiento,
- Una comparación de los demostradores de teoremas con los sitemas de cálculo simbólico basado en el estilo de interacción, la semántica y el rigor lógico,
- Una clasificación de la investigación en razonamiento automático según las siguientes características:
- IA vs. orientación lógica,
- automático vs. interactivo,
- búsqueda de la demostración vs. algoritmos específicos.
- Una clasificación de las aplicaciones del razonamiento automático en dos campos:
- verificación formal y
- formalización de las matemáticas.
Como ideas más interesantes destaco las siguientes:
- La combinación de sistemas de cálculo simbólicos y demostradores de teoremas usando los primeros como "oráculos".
- La posibilidad de verificar los traductores de problemas combinatorios a SAT. A partir de esta idea se creó el proyecto Verificación de traductores de problemas combinatorios en SAT.
José A. Alonso 10:38, 12 November 2008 (CET)
