Conceptos mas destacados de la clase teorica de hoy: regla de resolucion de Robinson y la forma clausal. En la clase de practica, hemos aprendido el concepto de predicado dinámico, muy útil para nuestro futuro videojuego
Teoria
- Fórmula satisfacible: una fórmula lógica es satisfacible si existe alguna interpretación que la hace verdadera.
- Fórmula insatisfacible: una fórmula lógica es insatisfacible si y sólo si es falsa para todas sus interpretaciones.
- Conjunto de fórmulas satisfacible: si existe una interpretación que es un modelo para todas las fórmlas del conjunto.
- Conjunto de fórmulas insatisfacible: si no existe ninguna interpretación que sea modelo (que haga verdadero el conjunto) para todas las fórmulas del conjunto .
Para estudiar si un razonamiento es o no correcto hay que averiguar si en conjunto de fórmulas es insatisfacible. Si lo es, entonces el razonamiento es correcto. Para deducir si el conjunto de fórmulas es insatisfacible hay que aplicar la regla de resolución, aunque, antes, hay que obtener la forma clausal de las premisas y de la negación de la conclusión.
FORMA CLAUSAL
Consiste en transformar fórmulas en otras fórmulas más simples de evaluar. Dichas fórmulas se caracterizan por la inexistencia del implicador. Una fórmula está escrita en forma clausal si dicha fórmula está representada por su conjunto de cláusulas.
- Cláusula: disyunción de literales.
- Literales: fórmula atómica afirmada o negada.
- Cláusula vacía: cláusula sin literales. Se representa por [] y su valor es siempre contradicción.
Para obtener la forma clausal de una fórmula hay que:
- Eliminar implicadores y coimplicadores mediante la aplicación de la regla:
A–>B = ¬AvB
- Normalizar negadores:
Leyes de Morgan: ¬(A v B) = ¬A ^ ¬B; ¬(A^B) = ¬A v ¬B.
- En fórmulas cuantificadas, en dos cuantificadores no deben coincidir los nombres de las variables.
- Eliminar los cuantificadores exitenciales.
- Poner los cuantificadores universales a la cabeza de la fórmula.
- Aplicar la regla distributiva:
A v (B ^C) = (A v B) ^ (A v C)
- Pueden coincidir constantes pero no las variables.
MÉTODO DE RESOLUCIÓN DE ROBINSON
La regla de resolución para una fórmula proposicional obtiene una nueva cláusula C3 a partir de otras dos, C1 y C2. Esta nueva cláusula es llamada resolvente de C1 y C2. Para hallar C3, C1 debe contener un literal L y C2 un literal ¬L. La cláusula C3 será la disyunción de todos los literales de C1 y de C2 menos los literales L y ¬L.
Ejemplos:
P y ¬P v Q C3=Q
P v Q y ¬P v Q C3=Q
P v Q y ¬P v ¬Q C3=Q v ¬Q ; P v ¬P (dos posibilidades)
¬P y P C3=nada
P v Q y ¬P v R C3=Q v R
Con todo esto, a partir de un conjunto de cláusulas C, si la cláusula resolvente es la cláusula vacía, C es insstisfacible, por tanto el razonamiento es correcto. Si no se encuentran cláusulas resolventes, C no es insatisfacible.
Practica
- Predicado dinámico: aquel que nos permite añadir cláusulas durante la ejecución del programa.
Para declarar un predicado dinámico:
Ejemplo: “:- dynamic mensaje_guardado/1.” esto es :- dynamic predicado/nº de argumentos.
Luego tenemos varios predicados dinámicos:
- assert : para añadir nuevos hechos.
- retract : para eliminar hechos. —–> retract(hecho(_)) : cuando dentro del paréntesis ponemos barra baja, elimina el primer hecho que encuentre.
- retractall : para borrar todos los hechos.
- listing: para ver las cláusulas del programa.
OPERADOR ->
Este operador “->” es un condicional. Por ejemplo a->c , es lo mismo que decir si ocurre a entonces c. Para a->c;e , significa si ocurre a entonces c, si no, e.
————————–
Bueno, pues ya esta!!!! hasta la semana que viene compañeros!!!!!! xD