RA2011: 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.