Lógicas para Aplicaciones Software Sub Lógicas para el Desarrollo de Programas Lógicas para la Ingeniería del Software Lógicas para la Ingeniería del Conocimiento y las BDs Lógicas para el Razonamiento aprox. y probabilistico Lógicas para la Concurrencia Lógicas para el Control y las Com. Lógicas para el Diseño de Lenguajes (e.g. visuales)
Algunos Ejemplos… Sub Lógicas para el Desarrollo de Programas L. Clausal Lógicas para la Ingeniería del Software L. Ecuacional Lógicas para la Ingeniería del Conocimiento y las BDs L. Modal Lógicas para el Razonamiento aprox. y probabilistico L. Probabilística Lógicas para la Concurrencia L. Temporal Lógicas para el Control y las Com. L. Lineal, L. Difusa Lógicas para el Diseño de Lenguajes (e.g. visuales) L. Pictórica
Sub Lógicas para el Desarrollo de Programas
Lógicas para la Ingeniería del Software
Lógicas para otras Aplicaciones Software Lógicas para Aplicaciones Software
IDEA TRADICIONAL:
LÓGICA usada como herramienta de representación de las propiedades de los programas y para razonar sobre éstas
(especificación, verificación y documentación del código)
I D E A O R I G I N A L !!!!!:
LÓGICA = LENGUAJE DE PROGRAMACIÓN
Lógicas para el Desarrollo de Programas:
P R O G R A M A C I Ó N D E C L A R A T I V A
ANALISIS DISEÑO IMPLEMENTAC. Programa
Ciclo de Vida Clásico VALIDACIÓN TEST – ? TEST – ? MANTENIMIENTO
ANALISIS Especific. IMPLEMENTAC. Programa (informal)
Ciclo de Vida con Prototipado MANTENIMTO. TEST – ? / ? VALIDACIÓN Prototipo PROTOTIPADO
ANALISIS Especific. OPTIMIZACIÓN REQUERIM. Formal MECÁNICA (Prototipo) .
Programación Automática VALIDACIÓN MANTENIMTO. Programa
Sub Lógicas para el Desarrollo de Programas
Lógicas para la Ingeniería del Software
Lógicas para otras Aplicaciones Software Lógicas para Aplicaciones Software
IDEA POPULAR:
Los Métodos Formales son lenguajes, técnicas y herramientas basados en las matemáticas (generalmente lógica y álgebra) y utilizados para especificar y verificar sistemas software
Lógicas para la Ingeniería del Software:
verificación si o no especificación
programa
Requisitos Datos Programas
(Gp:) Componentes Software Procesos Sofware
La Trilogía del Software:
Sub Lógicas para el Desarrollo de Programas
Lógicas para la Ingeniería del Software
Lógicas para otras Aplicaciones Software Lógicas para Aplicaciones Software
Lógicas para la Ingeniería del Conocimiento y las BDs Lógica modal: epistémica, temporal, dinámica, …
Lógicas para el Razonamiento aprox. y probabilistico Lógica geométrica, lógica probabilística
Lógicas para el Control y las Comunicaciones: Lógica lineal, lógica difusa
Lógicas para la Programación Visual Lógica diagramática, lógica pictórica
Lógicas para otras Áreas de Especialización en Software:
LOGICA DIFUSA (Fuzzy Logica )
*** una LOGICA Multivaluada (en vez de binaria) ***
En LÓGICA CLÁSICA: 0 or 1, blanco o negro, si o no; (en términos del ALGEBRA BOOLEANA: cada elemento está en un conjunto o en otro, pero no en ambos)
La LOGICA DIFUSA permite valores entre 0 y 1, tonos del gris, (pertenencia parcial a un conjunto)
Se usa para soportar el RAZONAMIENTO APROXIMADO en SISTEMAS EXPERTOS: inferencias lógicas sobre propiedades y relaciones imprecisas. EJEMPLOS: optimización automática del ciclo de lavado de una lavadora en función de la carga, cantidad de detergente, etc; control de ascensores, electrodomésticos, cámaras, instrumentación de automóviles, aeronaves y armamento nuclear.
Sub Los hechos pueden ser ciertos hasta un cierto grado
0.7 El agua está fría
En lógica difusa, las fórmulas tienen un valor de verdad entre 0 y 1
Aplicaciones en Control Difuso, Robótica, S. Expertos Lógica Difusa
Sub x elemento; S conjunto; Sx nº real entre 0 y 1 (denotando el grado en que x pertenece a S)
(A?B)x = max (Ax,Bx) (A?B)x = min(Ax,Bx) (?A)x = 1 – Ax
F conjunto de las proposiciones falsas;T verdaderas. t(p)= (1-Fp+Tp)/2 (verdad de p) t(?a) = 1 – t(a) t(a?b) = min(t(a),t(b)) t(a?b) = max(1-t(a),t(b))
Lógica Difusa (cont.)
Sub Nuevas conectivas lógicas (exponenciales):
! of course (copiado – replicación) ?? why not (borrado)
Separación en dos clases de las conectivas estándar : ? y ? (conjunción acumulativa y alternativa) ? y ? (disyunción directa y tensorial ) Lógica Lineal
Sub Una premisa, en lógica clásica, puede usarse tantas veces se quiera (A, A? B) ?? B … pero A es verdad aún
En la vida real, la implicación es causal —o (las condiciones se modifican tras su uso: acción, reacción) EJEMPLO: A gastar 100 ptas. en tabaco, B comprar “ducados”, C comprar “celtas” A —o B y A —o C NO IMPLICA A —o B ? C Lógica Lineal (cont.)
Sub Se cumple, en cambio: A —o B y A —o C IMPLICA A —o B & C
La conjunción & tiene carácter alternativo, pero NO es una disyunción! Se puede demostrar a la vez A & B—o A y A & B—o B (tampoco es un if_then_else)
APLICACIONES: Control de recursos (de máquina) A ‘está libre el canal A’ B, C procesos que pueden fluir por el canal
Lógica Lineal (cont.)
Sub Nuevas conectivas lógicas (cuantif. modales):
UNIVERSAL (always, necesidad) ?? EXISTENCIAL (sometimes, posibilidad)
para formalizar el tiempo, las creencias, etc..
Ejemplo: estudiante(A) ? ??profesional(A) Lógica Modal
Introducción a laLógica ModalMaría Alpuente Departamento de Sistemas Informáticos y Computación Universidad Politécnica de Valencia Camino de Vera s/n Apdo. 22.012 46.071 Valencia (España)
E.mail: [email protected] URL: http://www.dsic.upv.es/users/elp/alpuente.html
Lógicas no Estándar(Modificaciones y Extensiones de la Lógica Clásica) Lógica multi-valuada (N valores) Lógica Parcial Lógica Difusa Lógica Intuicionista Lógicas Modales MODIFICAN GENERALIZAN
Lógicas Modales GENERALIZAN la lógica clásica introduciendo dos conectivas lógicas adicionales (u operadores modales): UNIVERSAL (necesidad) ? EXISTENCIAL (posibilidad)
que permiten formalizar: la necesidad el tiempo las creencias, etc..
IDEA: la verdad es un concepto relativo que depende de los ‘mundos posibles’
Lógicas Modales (cont.) Interpretaciones A necesariamente es verdad A siempre será verdad A debe suceder A
cuando termina el programa, es verdad A
es conocido que A
se cree que se cumple A Interpretaciones ? A posiblemente es verdad A a veces será verdad A puede suceder A
existe una ejecución del programa que termina siendo A verdad no se conoce el opuesto de A no se cree que se cumple el opuesto de A
(? A =def ? ? A)
Lógicas Modales (cont.) Lógicas Temporales (lógicas del tiempo) A (always A) ? A (sometimes A) Lógicas Dinámicas(lógicas de la acción, lógica modal para razonar acerca de las acciones y procesos) Lógicas Epistémicas(lógicas del Conocimiento y dela Creencia/Ignorancia)
Lógicas Modales (cont.) Un marco de interpretación (frame) es un par F=(W,R) donde: W es un conjunto no vacío (Universo de puntos o mundos posibles) R es una relación binaria sobre W (Relación de accesibilidad)
Sea P un conjunto de fórmulas. Un modelo para P sobre un marco F=(W,R) es una terna M=(W,R,V) donde: V es una aplicación de P en 2W (el conjunto de los subconjuntos de W) que asigna a cada p ? P el subconjunto de puntos w ? W en los que p es verdad (TEORÍA DE MODELOS, caso proposicional)
Lógicas Modales (cont.) La relación ‘la fórmula A es verdad en el punto w en el modelo M’
(en símbolos M ?=w A) se define recursivamente como sigue:
? (M ?=w false) M ?=w p si w ? V(p) M ?=w (A????) si (M ?=w A?????M ?=w??) M ?=w A si wRt implica que M ?=t A para todo t ? W
(TEORÍA DE MODELOS, caso proposicional)
Lógicas Modales (cont.) ‘La fórmula A es verdad en el modelo M=(W,R,V) si es verdad en todos los puntos del modelo’ (M ?= A si M ?=w A para todo w ? W)
‘La fórmula A es verdad en el marco F=(W,R) si es verdad en cada modelo M=(W,R,V)’ (F?= A si M ?=A para todo M=(W,R,V))
‘La fórmula A es válida si es verdad en cada marco’ (?= A si F?= A para todo F) (TEORÍA DE MODELOS, caso proposicional)
Lógicas Modales (cont.) ‘La fórmula A es verdad en el mundo w si A es verdad en todos los mundos posibles accesibles desde w’.
‘La fórmula ?A es verdad en el mundo w si A es verdad en alguno de los mundos posibles accesibles desde w’. (TEORÍA DE MODELOS, caso proposicional)
Lógicas Multimodales Son lógicas cuyos lenguajes tienen más de un operador modal. Se utilizan colecciones de símbolos {[i] | i ? I} cada uno de los cuales corresponde a un operador universal Los operadores existenciales duales son < i> y se definen como ?[i]? si A es una fórmula, entonces [i]A e < i>A también lo son Un marco multimodal es F=(W, {Ri | i ? I}) donde las Ri son relaciones Ri ??W x W para cada i ? I M ?=w[i]A si w Ri t implica que M ?=t A para todo t ? W
Una Axiomatización de laLógica (Multi-)Modal El sistema axiomático más simple es K(a) (Prior 65): AXIOMAS: algún conjunto de axiomas de la lógica clásica K(a): ([a]A ^ [a](A ??B )) ? [a]B REGLAS DE INFERENCIA Modus Ponens Necesidad A |- [a] A Axiomas adicionales: D(a): [a]A ? < a>A T(a): [a]A ? A 4(a): [a]A ? [a][a]A 5(a): < a>A ? [a]< a>A B(a): A ? [a]< a>A G(a): [a]([a]A ??? ? [a]A ?(a): < a>A? [a]A
Lógicas del Tiempo TOPOLOGÍA del tiempo
discreto o continuo? (tiempo continuo: hay un momento entre cada dos) lineal, paralelo o ramificado? (cada rama corresponde a una posible historia del mundo. Puede haber ramificaciones en el futuro -pasado único-o también en el pasado -distintos pasados-) acotado o sin acotar? circular?
Lógicas del Tiempo (cont) TAXONOMIAS
Aproximación de primer orden-argumento extra para el tiempo- Aproximaciones modales Discrete & Linearly Ordered Time (next, since, until) Branching Time Dense Time Interval Logic
Lógicas Temporales La misma sentencia puede tener diferentes valores de verdad en distintos momentos del tiempo Los elementos de W son los momentos del tiempo sRt significa: s ocurre después de t (antes de t) A (always A) A será verdad en todos los tiempos futuros (A fue verdad en todos los tiempos del pasado) ? A (sometimes A) A será verdad en algún tiempo del futuro (A fue verdad en algún tiempo del pasado)
Lógica Dinámica Es una lógica multimodal Se asocia un operador modal [i] con cada instrucción i de un lenguaje de programación sRt significa: hay una ejecución del programa que empieza en s y termina en t [i] A (tras ejecutarse la instrucción i, es verdad A) < i> A (hay una ejecución de la instrucción i, que termina siendo verdad A) W es el conjunto de los distintos estados de un proceso computacional ________________ (L. dinámica simple:) A (cada ejecución del programa que termina acaba en un estado en el que es verdad A) ? A (hay alguna ejecución del programa que termina en un estado en el que es verdad A)
Lógica Dinámica (cont.) Se usa un conjunto de constructores dinámicos: composición secuencial (;) (con elemento neutro ID, el programa que no hace nada) unión (?) (elección indeterminista) repetición finita de un programa (*) ejecución inversa (-1) (t;t -1 es el programa que no cambia nada)
Axiomas adicionales: 1: [t;t’]A ? [t][t’]A 2: {ID}A ? A for {ID}=< ID>,[ID] 3: [t?t’]A ? [t]A^[t’]A 4: [t*]A ? A^ t[t*]A
Lógicas del Conocimiento y de la Creencia Los operadores modales se interpretan como conocimiento o creencia
A (se conoce A (se cree A)) ? A (no se conoce el opuesto de A (no se cree el opuesto de A))
Existen variantes multimodales
[i] A (el agente i conoce o cree A) < i> A (el agente i no conoce o no cree el opuesto de A)
Deducción Modal Automática Para automatizar la lógica modal es posible: desarrollar métodos de deducción modal traducir a otras lógicas (con teorías ecuacionales y sorts) Los resultados estándar (completitud, etc) son muy complejos en lógica modal: no existe una forma normal para las fórmulas modales ? (p ^q) el concepto de unificación se debe generalizar (e.g., p y ??p soncontradictorios, mientras que ?p y ??p no lo son) la contradicción puede estar sumergida varios niveles (e.g., ?p y ??p) o escondida en varias cláusulas (e.g., (p v q), ??p y ??q) los cuantificadores y operadores modales interaccionan
Traducción a lógica clásica T(w,p(t1,…,tn)) = p’(w,t1,…,tn) T(w,?A) = ?T(w,A) T(w,AvB) = T(w,A) v T(w,B) T(w,?xA) = ?xT(w,A) T(w,A) = ?w’(?R(w,w’) v T(w’,A)) Teorema. Sea L una logica multimodal. Sea A una fórmula cerrada. A es insatisfacible en L sii T(wo,A) es insatisfacible en lógica de primer orden.
Programación Lógica Modal y Temporal Modal Prolog (Molog) Temporal Prolog (MetaTem, Tempura)
IDEA. Extender HCL con conectivas modales o temporales:
Fp (en el futuro, p será siempre verdad) Pp (en el pasado, p fue siempre verdad) ?p = p v Fp v Pp p = ???p
Sintaxis de un Prolog Temporal Un programa es un conjunto de cláusulas Una cláusula es una cláusula ordinaria o una cláusula always Una cláusula always es p, donde p es una cláusula ordinaria Una cláusula ordinaria es una cabeza H o un H?? A, donde A es un cuerpo Una cabeza es un átomo o FA o PA, donde A es una conjunción de cláusulas ordinarias Un cuerpo es un átomo, una conjunción de cuerpos o un FA o PA, donde A es un cuerpo Un objetivo es un cuerpo
| Página siguiente |