LI2014

En la clase de hoy del curso de Lógica Informática se han comentado ejercicios de lógica de primer orden propuestos en exámenes de cursos anteriores. En concreto,

• del examen del segundo parcial del curso 2007-08 se han comentado los siguientes ejercicios:
  • El 2 para calcular la forma de Skolem y la clausal de una fórmula.
  • El 3 para calcular el universo de Herbrand de un conjunto de fórmulas y decidir su consistencia mediante resolución.
  • El 4 para formalizar un argumento y decidir su validez por resolución, tableros semánticos y deducción natural.
• del examen de la convocatoria de junio de 2008 se han comentado los siguientes ejercicios:
  • El 2 para formalizar expresiones que usan igualdad.

En la clase de hoy del curso de Lógica Informática” se ha presentado la resolución en la lógica de primer orden como ampliación del presentado en el tema 5
para la lógica proposicional.

Las principales diferencias se encuentran en la unificación, separación de variables y factorización.

Las transparencias de esta clase son las del tema 12
Read More “LI2014: Resolución en lógica de primer orden”

En la segunda parte de la clase de hoy del curso de Lógica Informática se ha estudiado cómo se puede puede reducir la consistencia de conjuntos de cláusulas de primer orden a la consistencia de conjuntos de cláusulas proposicionales.

En primer lugar, se ha observado que la reducción es inmediata en el caso de fórmulas sin variables.

A continuación se han presentado procedimientos para construir los universos de Herbrand, las bases de Herbrand y las interpretaciones de Herbrand. Así como un procedimiento que transforma modelos de conjuntos de cláusulas en modelos de Herbrand. Por tanto, la consistencia de un conjunto de cláusulas se reduce a la búsqueda de modelos de Herbrand.

Finalmente, se ha explicado el teorema de Herbrand y su aplicación para decidir la consistencia de un conjunto de cláusulas buscando un subconjunto finito de su extensión de Herbrand que sea consistente (en el sentido proposicional).

Las transparencias de la clase son las del tema 11.

En la primera parte de la clase de hoy del curso de Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra G que no tenga cuantificadores, que esté en forma normal conjuntiva y que sea equisatisfacible con F (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem. A partir de las formas se Skolem se obtienen las formas clausales.

Las transparencias de esta clase son las del tema 10