Estoy interesado en esta cuestión, pero no voy a enumerar mis conocimientos/demandas sino que voy a orientarlo a un propósito más general; así que lo primero se refiere a los requisitos previos, es decir
¿Cuántos conocimientos teóricos (lógica matemática, programación y otros) hay que tener antes de dedicarse a la demostración automática de teoremas (ATP)? ¿Hay algún campo de la lógica matemática que no sea un prerrequisito necesario pero que proporcione una visión más profunda del ATP?
Una vez cumplidos los requisitos previos, sólo hay que sumergirse:
¿Cómo se empieza con la ATP? ¿Existen libros, apuntes de clase, que expliquen los conceptos cruciales? Una vez que uno ha terminado con la idea general de ATP, ¿cómo se procede a hacer ¿a qué se debe?
Sin embargo, uno podría estar preocupado (al menos esa es mi principal preocupación) por la gran cantidad de teoremas diferentes; cómo se elige, y existe la posibilidad de que si uno elige el equivocado, se quede con un conocimiento obsoleto (incluso en términos de matemáticas puras). En otras palabras
¿Hasta qué punto hay que preocuparse por el "envejecimiento" de los teóricos? ¿Existen enfoques agnósticos del lenguaje?
