Semana 6

Variables libres y ligadas

En esta semana nos toco escoger un problema del siguiente pdf y realizarlo:
Liga del pdf: http://www.logicinaction.org/docs/ch4.pdf


Ejercicio a realizar:


Exercise 4.27 Give the bound occurrences of x in the following formula.
∃x(Rxy v Sxyz) ^ P x

Traducción:

Dar a las ocurrencias ligados de x en la fórmula siguiente.
∃x(Rxy v Sxyz) ^ P x

Antes para poder ver mejor el problema sacamos su árbol o estructura:

En la primera sentencia con tres ocurrencias: "∃x(Rxy v Sxyz) " estan ligados x1, x2 y x3, por un cuantificador existencial

Segunda sentencia que es "Px" X es completamente libre de los demás ya  que no es en el ámbito de un cuantificador al igual que sus acompañantes "yz"

Referencia y ligas de interés:
http://en.wikibooks.org/wiki/Formal_Logic/Predicate_Logic/Free_and_Bound_Variables
http://en.wikipedia.org/wiki/Free_variables_and_bound_variables

Logica predicativa

Aquí el ejercicio que me toco hacer para Verificación y Validación

"Some eggs are hard-boiled;

No eggs are uncrackable"

"Algunos huevos son duros;

No hay huevos que son irrompibles"

E(x) = eggs

H(x) = hard-boiled

U(x) = uncrackable

are = ->

Algo de teoría:

Some eggs are hard-boiled:

No eggs are uncrackable:

Entonces:

Si algunos no son duros y no rompibles no son huevos

BDD

En esta semana nos toco realiza las siguientes actividades:

1-. Crear una expresión Booleana

2-. Realizar un BDD con la misma

3-. Reducir el BDD a un ROBDD

La expresión Booleana a verificar es la siguiente:

y(x) = [(a^b)^(bvc)]v(c^¬a)

Aquí esta la tabla de la verdad:

Posteriormente pasamos a crear la BDD, e aquí como quedo:

Posteriormente la reducimos:

Aquí una pequeña animación de como se fue reduciendo:

Ahora veamos el ROBDD con el siguiente orden  c<a<b para verificar si se redujo mas, al parecer se redujo un nodo mas: