Diferencia entre revisiones de «A short survey of automated reasoning»
(New page: 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''. Spr...) |
|||
| 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: | ||
| + | # 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. | ||
Revisión del 08:06 22 oct 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.
