domingo, 16 de septiembre de 2012

Principios de demostraciones de validez

Esta es mi tarea 5 correspondiente a la clase de validación y verificación de Software. La tarea consistió en elegir un ejercicio del pdf logicination y resolverlo, el mio es el 4.18 sobre Fórmulas, situaciones e imágenes donde con una imagen podemos representar diferentes semánticas. 

Exercise 4.18 Consider the following picture:


Use G for the property of being a girl, H for the property of being a hat, and W for the relation of wearing (so that W xy expresses that x is wearing y). Now do the following:

(1) Give a predicate logical formula that is true for the situation in the picture.
(2) Give a predicate logical form

Ejercicio 4.18 considere la siguiente imagen, utilice:
  • G para la propiedad de ser una chica, 
  • H para la propiedad de ser un sombrero 
  • W para la relación de usando (para W(xy) expresa que x está usando y).
Ahora lo siguiente:

(1) Dar una fórmula de lógica predicada que es cierto para la situación en la imagen.

Para esta parte también utilizaremos nuevamente los cuantificadores, en este caso solo utilice uno de la siguiente manera:
  • : Todos, para todos
  • En la imagen se muestran diferentes enunciados que podrían representarse por lógica predictiva, esta es una de ellas: 
  • Todas las chicas están usando sombrero 
      x(Gx ^Hy ^Wxy)
(2) Dar una fórmula lógica predicada que es falsa por la situación en la imagen
  • Algunas chicas no usan sombrero.  
 Gx(¬Wxy->Hy )
 
 

domingo, 9 de septiembre de 2012

Lógica predictiva

En esta semana la tarea a entregar es sobre lógica predictiva(predicados) o lógica de primer orden, dentro del libro "Symbolic Logic" debíamos escoger proposiciones compuestas y obtener de ahí lo que son las proposiciones de lógica predictiva.

Esté es mi par de proposiciones:
  • Some pictures are not first attempts;(Algunas imágenes no son los primeros intentos)
  • No first attempts are really good.(Ninguno de los primeros intentos son  buenos)
Las expresiones que utilice son las siguientes:
  • F(x)= imágenes 
  • G(x)= primeros intentos
  • H(x)= son buenos
Expresiones:
Se  utilizan los cuantificadores para expresar el conjunto de proposiciones.
  • : Todos, para todos 
  • : Por lo menos uno, algunos, algunas
Ahora las proposiciones de lógica predictiva son las que se muestran enseguida:
  • F(x) -> ¬G(x)
  • ¬G(x) -> H(x)
Como ninguno fue un intento bueno, algunas imágenes no son buenas. 
  • Conclusión:  F(x)-> ¬H(x).

martes, 4 de septiembre de 2012

Tarea 4.Diagramas Binarios de Decisión

Para esta tarea el problema a resolver es:
  • Inventen una expresión Booleana(Usando por mínimo 3 variables y 4 conectivos básicos)
  • Construyan y dibujen su BDD.
  • Reduzcan el BDD resultante a un ROBDD.
  • Dibujen el ROBDD resultante.
BDD (Diagrama de Decisión Binario)
Un diagrama de decisión binario (DDB) es un grafo acíclico dirigido con
Uno o dos nodos terminales etiquetados con 0 o 1

Expresión Booleana
Mi expresión a representar es la siguiente:
(x2 ^ x3) v (x1 ^ x3)

Tabla lógica:

Árbol Binario de Decisión: 


BDD: 
Este es mi Diagrama de Decisión Binario que dio como resultado.  


Reducción a ROBDD y ROBDD resultante 
En el PDF: "An Introduction to Binary Decision Diagrams" por Henrik Reif Andersen, se mencionan tres condiciones para el orden y reducción:
  • Las variables deben estar ordenadas
  • Los nodos deben ser únicos
  • Solo tests no redundantes deben estar presentes

Referencias: 
"An Introduction to Binary Decision Diagrams"