RA2011: Semántica de la lógica de primer orden

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha presentado la semántica de la lógica de primer orden.

Hemos empezado viendo ejemplos para ver de qué depende la verdad de una fórmula: del universo, de la interpretación de los símbolos constantes y de la asignación a las variables libres.

A partir de estos ejemplos, se introduce los conceptos de

  • estructura {\cal I} (formadas por un universo U junto con la interpretación I de las constantes, funciones y relaciones),
  • asignación a las variables en una estructura (A) e
  • interpretación (formada por una estructura junto con una asignación)

A continuación, se definen los siguientes conceptos:

  • valor de un término en una interpretación ({\cal I}_A(t)),
  • valor de ua fórmula en una interpretación ({\cal I}_A(F)),
  • realización de una fórmula ({\cal I}_A \models F),
  • satisfacibilidad de una fórmula en una interpretación,
  • validez de una fórmula en una estructura ({\cal I} \models F),
  • modelo de una fórmula ({\cal I} \models F),
  • satisfacibilidad de una fórmula,
  • validez de una fórmula (\models F),
  • realización de un conjunto de fórmulas ({\cal I}_A \models S),
  • consistencia de un conjunto de fórmulas,
  • modelo de un conjunto de fórmulas ({\cal I} \models S),
  • consecuencia lógica (S \models F),
  • equivalencia lógica (F \equiv G),

También se ha estudiados las relaciones entre los anteriores conceptos.

Las transparencias de la clase son las páginas 23 a 51 del tema 1.

RA2011: Introducción a la lógica de primer orden

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha comenzado el estudio de la lógica de primer orden.

En primer lugar hemos visto cómo se puede usar la lógica de primer orden para la representación de conocimiento. Como ejemplo hemos visto la representación del mundo de los bloques y su uso en problemas de planificación.

Basándonos en los ejemplos anteriores hemos introducido la sintaxis de la lógica de primer orden, resaltando la naturaleza recursiva de las definiciones.

Las transparencias de la clase son las 23 primeras del tema 1.

RA2011: Introducción al razonamiento automático

PorJosé A. Alonso

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?.