Next: Ejemplo del procedimiento de
Up: Resolución: un procedimiento de
Previous: Prueba
- eliminar implicaciones:
equivale a 
- mover las negaciones: las negaciones de átomos se permiten sólo en CNF y no en INF, se mueven con las leyes de Morgan, las equivalencias de cuantificadores y la doble negación
- normalizar las variables:
, en sentencias de este tipo en las que se usa el mismo nombre de variable, cambiar los nombres - mover los cuantificadores a la izquierda sin cambiar el significado de la sentencia
equivale a 
- skolemization: quitar los cuantificadores existenciales
en el caso sencillo con la regla de eliminación del existencial
si es necesario con funciones de Skolem
la regla de eliminación del existencial no vale:
la variable cuantificada existencialmente se reemplaza por un término que consiste en una función de Skolem (debe ser un nombre de función que no exista en la KB) aplicada a todas las variables cuantificadas universalmente fuera del cuantificador existencial en cuestión:
- distribuir los
sobre los 
equivale a 
- eliminar conjunciones o disyunciones anidadas:
equivale a 
despues de estos 7 pasos una sentencia está en CNF - conversión a INF: reunir los literales negativos y los literales positivos y construir la implicación
equivale a 
Alvaro Barreiro Garcia
Thu Jul 18 18:35:01 MET DST 1996