A short survey of automated reasoning

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:

1. Una breves historia de la automatización del razonamiento,
2. 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,
3. Una clasificación de la investigación en razonamiento automático según las siguientes características:
   1. IA vs. orientación lógica,
   2. automático vs. interactivo,
   3. búsqueda de la demostración vs. algoritmos específicos.
4. Una clasificación de las aplicaciones del razonamiento automático en dos campos:
   1. verificación formal y
   2. formalización de las matemáticas.

Como ideas más interesantes destaco las siguientes:

1. La combinación de sistemas de cálculo simbólicos y demostradores de teoremas usando los primeros como "oráculos".
2. 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.