4.2 Forma de Skolem

Recordemos que una fórmula está en CNF si y solo si es una conjunción de disyunciones de literales.

Una fórumula está en PRENEX CONJUNTIVE NORMAL FORM (PCNF) si y solo si se encuentra de la sigueinte manera:

donde

son cuantificadores y
es una fórmula libre de cuantificadores en CNF. La secuencia
es llamada el prefijo y
es denominada matriz.

Una formula cerrada está en forma clausal si y solo si esta en PCNF y su prefijo consiste solo de cuantificadores universales (

). Una literal es una fórmula atómica o la negación de una fórmula atómica. Una clausula es una disyuncion de literales.

La siguiente fórmula está en forma clausal:

Puede ser escrita con la siguentes formas de notación abreviada:

Dada una fórmula cerrada A, entonces existe una fórmula

en forma clausal tal que
.

Enseguida se presenta un algoritmo para transformar una fórmula

a una fórmula
en forma clausal y así probar que
. La descripción de la transformación va a compañado por el desarrollo de un ejemplo usando la siguiente fórmula:

Algoritmo de Skolemizacion.

Entrada: Una formula cerrada A de cálculo de predicados

Salida: una fórmula

en forma clausal tal que
.

  • Renombrar las variables atadas de tal manera que una variable no aparezca en dos cuantificadores.
  • Quitar los operadores
    usando:
  • Meter las negaciones dentro de los cuantificadores usando:
  • Usar las leyes de De Morgan para meter las negaciones que afecten a paréntesis.
  • Eliminar las doble negación usando la equivalencia:
    .
  • Sacar los cuantificadores usando:
donde:
  • Usar la ley distributiva para transformar la matriz a CNF usando:
  • Quitar cuantificador existencial (
    )
    • Si no hay cuantificador universal (
      ) antes: lo quito y pongo una constante que no existe.
    • Si hay cuantificador universal (
      ) antes, usamos una función que dependa de las variables que poseen los cuantificadores universales.
    Resultado despues de el algoritmo de Skolem
<=Regresar Tema 4.1 Universo de Herbrand
=>Siguiente Tema: 4.3 Resolucion en Logica de Primer Orden
Regresar al TEMARIO: Matematicas Para Maestria

Búsqueda personalizada

GFDL