Archivo por autor

RA2011: Patrones de inducción en Isabelle: casos, inducción y otros

En la clase de hoy del curso de Razonamiento automático se han presentado los principales patrones de inducción en Isabelle: en la primera parte se ha presentado los patrones de de mostración por casos y por inducción y en la segunda parte se han presentado otros patrones (eliminación de disyunción, negación, contradicción y equivalencias).

La primera parte de la clase se ha basado en la siguiente teoría Isabelle
Leer el resto de esta entrada »

Formas normales, cláusulas y teorema de Herbrand

En la clase de hoy del curso de Razonamiento automático se ha estudiado:

  • la transformación de la formas a formas normales prenexas, formas de Skolem y forma clausal,
  • las interprestaciones de Herbrand,
  • el teorema de Herbrand y
  • el procedimiento de semidecisión basado en el teorema de Herbrand.

Las transparencias de la clase son las páginas 52 a 90 del tema 1.

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

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

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: Panorama del razonamiento automático mediante Otter, ACL2, PVS e Isabelle

En la clase de hoy del curso de Razonamiento automático se presentado una visión panorámica del razonamiento automático a través de ejemplos con los sistemas de razonamiento Otter/Mace, ACL2, PVS e Isabelle/HOL.

Las transparencias de la clase son
Leer el resto de esta entrada »