martes, 28 de agosto de 2012

Aplicaciones de logica propocional

Una de las formas de definir la lógica proposicional es como lo vimos en clase anteriormente es el estudio de las formas de razonamiento donde su validación depende solamente de las propiedades verdadero o falso.

De manera informal, una proposición se define como una frase que puede ser considerada
Verdadera y que no se puede descomponer en otras frases Verdaderas o Falsas, y estas a su ves pueden ser simples o compuestas.

Ejemplo: 
Luis es inteligente y estudioso = Proposición Compuesta
Llueve si y solo si esta nublado = Proposición Compuesta
Luis es inteligente = Proposición simple

Para poder relacionar distintas proposiciones se utilizan los conectivas como las siguientes:
Existe un lenguaje para la logica proposicional representado por el siguiente conjunto de simbolos: 




Existe un orden de precedencia entre los operadores: ¬, ∧, ∨, ⇒y⇔ 
  
Cada uno de los conectores o constantes lógicas se define semánticamente mediante
una tabla de verdad que muestra sus posibles valores veritativos según los casos. 
Aplicaciones:
Se necesita tener un lenguaje con una sintaxis y semántica bien definida.
Se puede utilizar dentro de las matematicas como:
  • Definición de objetos matemá́ticos: conjunto, números naturales, nú́meros reales.
  • Definición de teorías matematicas: teoria de conjuntos, teoria de los numeros naturales. 
En Circuitos logicos:
La aplicación de la logica proposicional es dentro de circuitos electricos  digitales y es posible en virtud del isomorfismo a la relación de igualdad que existe entre dos objetos.




Teoria de la computación: complejidad descriptiva, y algoritmos de aproximación.
    
En Inteligencia Artificial:
Representación de conocimiento, razonamiento con sentido comú́n.
Referencias: 
Aplicaciones de la logica proposicional 
Conceptos principales
Logica-Proposicional-para-Informitica
Clases lógica
circuitos-lgicos-presentation

martes, 21 de agosto de 2012

Lógica proposicional; formas normales

Tautología
Una expresión lógica es una tautología si es verdadera para todas las asignaciones posibles.

Nota: 
Si P → Q es una tautología se le llama implicación y se escribe P ⇒Q
Si P ↔ Q es una tautología se dice que es una doble implicación, se escribe P ⇔ Q






La validez es parte de una tautología ya que se da en el razonamiento y puede realizarse mediante las tablas de verdad.


Tarea 2. Ejemplo de Tautología
Aquí esta mi tautología esta esta dada por 3 variables de entrada p,q y r, para realizarla primeramente declare las proposiciones estas son compuestas ya que contienen conectivos lógicos. 

Premisas

P1= p ->q
P2=r -> q
P3 = p V r -> q
PT= q
 Tabla de verdad
 


Referencias:
www.fdi.ucm.es/profesor/rmartine/.../logica_tema1_4.pd

lunes, 13 de agosto de 2012

Introducción a la verificación formal

La prueba de software se conoce también como verificación y validación (V&V).
Es asegurar que el sistema de software cumpla las necesidades del usuario
 
Diferencias: 
  • Verificación: 
Se conoce como un conjunto de actividades que aseguran que el software implementa correctamente una función especifica, esto nos lleva a cuestionar, ¿Estamos construyendo el producto correctamente?. El software debe estar conforme a las especificaciones.
  • Validación:  
¿Se esta construyendo el producto adecuado?"El software debe hacer lo que el usuario requiere. 

Verificación estática y dinámica
  •  Verificación dinámica: Se refiere al ejercicio y observación del comportamiento del producto (prueba). 
  • Verificación estática: Se refiere al análisis de la representación estática del sistema para descubrir problemas. 
Los procesos de validación y verificación se inician con revisiones de requerimientos, luego se realizan revisiones del diseño e inspecciones de código hasta llegar a la prueba del producto.

El objetivo del proceso de V&V es garantizar la seguridad de que el sistema software esta “hecho para un propósito “, lo cual significa que el sistema debe ser suficientemente bueno para su uso establecido.
  
Pruebas de programas 
Las técnicas dinámicas también conocidas como testing(prueba) se basa en ejercitar una implementación. 
  • Puede revelar la presencia de errores no su ausencia
  • Una prueba exitosa consiste en descubrir uno o mas errores
  • Solo se considera la técnica de validación para requerimientos no-funcionales
  • De se usada en conjunto con la verificación estática 
  •  Pruebas estadística: Pruebas diseñadas para reflejar la frecuencia de las entradas del usuario.Usadas para estimación de la confiabilidad. 
  • Prueba de defectos: Pruebas diseñadas para descubrir defectos en el sistema. Una prueba de defectos exitosa es aquella que revela la presencia de defectos en el sistema.  
Depuración 
  • La prueba de defectos y la depuración son distintos procesos
  • La prueba de defectos se refiere a la confirmación de la presencia de errores
  • La depuración se refiere a la localización y reparación de estos errores.
  • La depuración involucra la formulación de una hipótesis acerca del comportamiento del programa y la prueba de la hipótesis para encontrar los errores en el sistema.  
Fases de pruebas
  • Pruebas de unidades: prueba de componentes individuales. 
  • Pruebas de módulos: prueba de conjuntos de componentes dependientes.
  • Pruebas de sub-sistemas: prueba de colecciones de módulos integrados en sub-sistemas.
  • Prueba del sistema: prueba del sistema completo ante de su entrega
  • Prueba de aceptación: pruebas de los usuarios para verificar que el sistema cumple con los requerimientos. Llamado en ocasiones prueba alfa.  
Ejemplos de mala validación.

1. Marinero sin rumbo (1962)
 
Coste: 18,5 millones de dólares.

Desastre:
El cohete Mariner 1, en una investigación espacial destinada a Venus, se desvió de su trayectoria de vuelo poco después de su lanzamiento. El control de la misión destruyó el cohete pasados 293 segundos desde el despegue.

Causa:
Un programador codificó incorrectamente en el software una fórmula manuscrita, saltándose un simple guión sobre una expresión. Sin la función de suavizado indicada por este símbolo, el software interpretó como serias las variaciones normales de velocidad y causó correcciones 
erróneas en el rumbo que hicieron que el cohete saliera de su trayectoria.  El fallo del Pentium en las divisiones largas (1993)
 


Coste: 475 millones de dólares, credibilidad de Intel.

Desastre: el promocionadísimo chip de Intel, Pentium, producía errores al dividir números en coma flotante que se encontraban en un rango determinado. Por ejemplo, dividiendo 4195835,0/3145727,0 se obtenía 1,33374 en lugar de 1,33382, un error del 0,006%. Aunque el error afectaba a pocos usuarios, se convirtió en una pesadilla en cuanto a sus relaciones públicas; con unos 5 millones de chips en circulación, Intel ofreció reemplazar los Pentium sólo de aquellos clientes que demostraran que necesitaban alta precisión en sus cálculos. Finalmente, reemplazó los chips de todos los que lo solicitaron.

Causa: El divisor en la unidad de coma flotante contaba con una tabla de división incorrecta, donde faltaban cinco entradas sobre mil, y que provocaba estos errores en los redondeos. 
Referencias:  
Validación y Verificación  
Pruebas