Meses: noviembre 2011

Hoy ha sido la 1ª la clase de Razonamiento automático. En esta clase se ha hecho una introducción al campo del razonamiento automático a partir la descripción realizada por Larry Wos en el primer número del Journal of Automated Reasoning:

El razonamiento automático se dedica a estudiar cómo usar un ordenador para ayudar en la parte de resolución de problemas que requiere razonamiento.

Algunas cuestiones que surgen durante dicho estudio son la representación del conocimiento, las reglas para derivar nuevo conocimiento del que se tiene, y las estrategias para controlar dichas reglas.

Otras cuestiones se refieren a la implementación de la teoría resultante y a las aplicaciones para las cuales el correspondiente software puede ser usado.

Teoría, implementación y aplicaciones juegan papeles vitales para el razonamiento automático a la hora de intentar alcanzar uno de sus principales objetivos: proporcionar un asistente de razonamiento automático.

También se ha comentado distintos sistemas de razonamiento, metodología de su utilización y aplicaciones.

Como primera aplicación importante se ha comentado la demostración de la conjetura de Robbins que constituye el primer teorema importante demostrado por una máquina ante que los humanos pudieran demostrarlo. Esta era una de las promesas de la inteligencia artificial. Para ver su papel dentro de la I.A. hemos terminado la clase comentando la historia de la inteligencia artificial.

Las transparencias usadas en clase son las 6 primera del tema 0.

Como tarea para la próxima clase se propuso la lectura del artículo de G. Sutcliffe What is automated theorem proving?.