Download Transparencias Lógicas Software - DSIC

Lógicas para Aplicaciones Software
María Alpuente Frasnedo
Depto. de Sistemas Informáticos y Computación
U. Politécnica de Valencia
http://www.dsic.upv.es/~alpuente.html
Desarrollo de
Programas
Ingeniería de
Software
Bases de
Datos
Ingeniería de
Conocimiento
Procesamiento
de Lenguajes
Inteligencia
Artificial
Comprensión
L. Natural
Sistemas
Operativos
Lógica y Bases de Datos
• Lenguaje de Definición de Datos
• Lenguaje de Actualización
• Lenguaje de Interrogación
• Comprobación de Restricciones de Integridad
MODELO RELACIONAL = REPRESENTACION POR TABLAS
Nombre
Cargo
Paloma
Claudia
Gonzalo
Presidenta
Secretaria
Tesorero
Cuotas
1000
1000
1000
Fecha Nacim.
3/1/94
12/11/99
12/11/99
Fecha Ingreso
3/1/94
12/11/99
12/11/99
Club(Paloma, Presidenta, 1000, 3/1/94, 3/1/94)
Club(Claudia, Secretaria, 1000, 12/11/99, 12/11/99)
Club(Gonzalo,Tesorero, 1000, 12/11/99, 12/11/99)
LENGUAJES DE CONSULTA RELACIONAL =
SIMBOLISMO DEL CP 1 Orden
Club
Nombre
Cargo
Paloma
Claudia
Gonzalo
Presidenta
Secretaria
Tesorero
Dirección
Cuotas
1000
1000
1000
Nombre
Calle
Paloma
Claudia
Gonzalo
Dr. Palos
Dr. Palos
Vechia
Tramvia
Fecha Nacim.
Fecha Ingreso
3/1/94
12/11/99
12/11/99
3/1/94
12/11/99
12/11/99
Número
Ciudad
7
7
7
Sagunto
Sagunto
Pisa
?- Club(x,y,z,u,v), Dirección(x,’Dr. Palos’,n,c)
( Cálculo Relacional de Tuplas)
BD = Interpretación de una teoría lógica
BD “Deductiva” = Teoría lógica
Club(Paloma, Presidenta, 3/1/94)
Club(Claudia, Secretaria, 12/11/99)
Club(Gonzalo,Tesorero, 12/11/99)
Cuota(x,1000)  Club(x,y,z)
Ingreso_Club(x,z)  Club(x,y,z)
Desarrollo de
Programas
Ingeniería de
Software
Bases de
Datos
Ingeniería de
Conocimiento
Procesamiento
de Lenguajes
Inteligencia
Artificial
Comprensión
L. Natural
Sistemas
Operativos
Lógicas para Aplicaciones Software
 La lógica proporciona una formulación
simbólica e independiente del dominio
de las leyes del pensamiento humano
 Este doble carácter de la lógica hace posible
mecanizar sus técnicas y métodos
Lógicas para Aplicaciones Software
(cont.)

PROBLEMA:



La lógica clásica se desarrolló para estudiar objetos matemáticos
bien definidos, consistentes e inmutables -carácter estáticoSus nuevas aplicaciones requieren formas más dinámicas
(y menos perfectas) de lógica
Los métodos de la lógica, en general, resultan caros en términos
computacionales -> es necesario reducir sus costes sin perder sus
buenas propiedades lógicas
Lógicas para Aplicaciones Software
(cont.)

SOLUCIÓN: Lógica Computacional
(Lógicas para Aplicaciones Software)
Lógicas con la expresividad y la potencia computacional adecuadas para:


Modelar el conocimiento impreciso, incompleto, contradictorio,
revisable, dinámico, distribuido...
Razonamiento no monótono, aproximado, probabilístico...
Lógicas para Aplicaciones Software
 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...
 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ó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)
L. Modal
L. Probabilística
L. Temporal
L. Lineal, L. Difusa
L. Pictórica
Lógicas para Aplicaciones Software
 Lógicas para el Desarrollo de Programas
 Lógicas para la Ingeniería del Software
 Lógicas para otras Aplicaciones Software
 Lógicas para el Desarrollo de Programas:
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
PROGRAMACIÓN
DECLARATIVA
Ciclo de Vida Clásico
MANTENIMIENTO
ANALISIS
VALIDACIÓN
DISEÑO
TEST - 
IMPLEMENTAC.
TEST - 
Programa
Ciclo de Vida con Prototipado
ANALISIS
Especific.
IMPLEMENTAC.
Programa
(informal)
TEST -  / 
PROTOTIPADO
MANTENIMTO.
VALIDACIÓN
Prototipo
Programación Automática
ANALISIS
REQUERIM.
Especific.
Formal
(Prototipo)
.
VALIDACIÓN
MANTENIMTO.
OPTIMIZACIÓN
MECÁNICA
Programa
Lógicas para Aplicaciones Software
 Lógicas para el Desarrollo de Programas
 Lógicas para la Ingeniería del Software
 Lógicas para otras Aplicaciones Software
 Lógicas para la Ingeniería del 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
especificación
programa
verificación
si o no
La Trilogía del Software:
Requisitos
Datos
Componentes Software
Procesos Sofware
Programas
Lógicas para Aplicaciones Software
 Lógicas para el Desarrollo de Programas
 Lógicas para la Ingeniería del Software
 Lógicas para otras Aplicaciones Software
para otras Areas de
ación en 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
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.
Lógica Difusa
 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 (cont.)
 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 Lineal
 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 (cont.)
 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.)
 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
B, C
‘está libre el canal A’
procesos que pueden fluir por el canal
Lógica Modal
 Nuevas conectivas lógicas (cuantif. modales):
• UNIVERSAL
(always, necesidad)
 EXISTENCIAL (sometimes, posibilidad)
para formalizar el tiempo, las creencias, etc..
 Ejemplo: estudiante(A)   profesional(A)
Introducción a la
Lógica Modal
Marí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:
URL:
[email protected]
http://www.dsic.upv.es/users/elp/alpuente.html
Lógicas no Estándar
GENERALI
ZAN
MODIFIC
AN
(Modificaciones y Extensiones
de la Lógica Clásica)
n
Lógica multi-valuada (N valores)
Lógica Parcial
Lógica Difusa
Lógica Intuicionista
n
Lógicas Modales
n
n
n
Lógicas Modales
n
la lógica clásica introduciendo dos conectivas
lógicas adicionales (u operadores modales):
GENERALIZAN
u
u
• UNIVERSAL (necesidad)
◊ EXISTENCIAL (posibilidad)
que permiten formalizar:
u
u
u
n
la necesidad
el tiempo
las creencias, etc..
IDEA: la verdad es un concepto relativo que depende de los ‘mundos
posibles’
Lógicas Modales (cont.)
(◊ A =def •  A)
n
n
necesariamente es verdad A
siempre será verdad A
debe suceder A
n
cuando termina el programa, es verdad A
n
es conocido que A
n
n
Interpretaciones ◊ A
Interpretaciones •A
n
n
n
n
n
n
n
se cree que se cumple 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
Lógicas Modales (cont.)
n
Lógicas Temporales
(lógicas del tiempo)
u •A (always A)
u ◊ A (sometimes A)
n
Lógicas Dinámicas
(lógicas de la acción, lógica modal para
razonar acerca de las acciones y procesos)
n
Lógicas Epistémicas
(lógicas del Conocimiento y de
la Creencia/Ignorancia)
Lógicas Modales (cont.)
(TEORÍA DE MODELOS, caso proposicional)
n
n
n
n
n
n
n
n
n
n
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)
Lógicas Modales (cont.)
(TEORÍA DE MODELOS, caso proposicional)
n
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:
F
F
F
F
 (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
Lógicas Modales (cont.)
(TEORÍA DE MODELOS, caso proposicional)
n
‘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))
n
n
‘La fórmula A es válida si es verdad en cada marco’
(= A si F= A para todo F)
Lógicas Modales (cont.)
(TEORÍA DE MODELOS, caso proposicional)
n
n
‘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’.
Lógicas Multimodales
n
n
n
n
n
n
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 la
Lógica (Multi-)Modal
n
El sistema axiomático más simple es K(a) (Prior 65):
u
AXIOMAS:
F
F
u
REGLAS DE INFERENCIA
Modus Ponens
F Necesidad A |- [a] A
Axiomas adicionales:
F D(a): [a]A  <a>A
F T(a): [a]A  A
F 4(a): [a]A  [a][a]A
F
n
algún conjunto de axiomas de la
lógica clásica
K(a): ([a]A ^ [a](A B ))  [a]B
Lógicas del Tiempo
n
TOPOLOGÍA del tiempo
n
discreto o continuo?
u
n
lineal, paralelo o ramificado?
u
n
n
(tiempo continuo: hay un momento entre cada dos)
(cada rama corresponde a una posible historia del mundo.
Puede haber ramificaciones en el futuro -pasado únicoo también en el pasado -distintos pasados-)
acotado o sin acotar?
circular?
Lógicas del Tiempo (cont)
TAXONOMIAS
n
n
Aproximación de primer orden
-argumento extra para el tiempoAproximaciones modales
u
u
u
u
Discrete & Linearly Ordered Time
(next, since, until)
Branching Time
Dense Time
Interval Logic
Lógicas Temporales
n
n
n
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)
u • A (always A)
u
A será verdad en todos los tiempos futuros
(A fue verdad en todos los tiempos del
pasado)
u ◊ A (sometimes A)
Lógica Dinámica
n
n
n
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
u [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
u ________________ (L. dinámica simple:)
u • A (cada ejecución del programa que termina
u
n
Lógica Dinámica (cont.)
n
Se usa un conjunto de
constructores dinámicos:
u
composición secuencial (;)
(con elemento neutro ID, el
programa que no hace nada)
u
u
u
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)
n
Axiomas adicionales:
F
1: [t;t’]A  [t][t’]A
Lógicas del Conocimiento y
de la Creencia
n
Los operadores modales se interpretan como
conocimiento o creencia
u
u
n
• 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
u
u
[i] A (el agente i conoce o cree A)
<i> A (el agente i no conoce o no cree
Deducción Modal Automática
n
Para automatizar la lógica modal es posible:
u 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:
u no existe una forma normal para las
fórmulas modales ◊ (p ^q)
u el concepto de unificación se debe
generalizar (e.g., •p y ◊p son
contradictorios, mientras que
◊p y ◊p no lo son)
u la contradicción puede estar sumergida varios niveles (e.g.,
◊•p y •◊p) o
escondida en varias cláusulas
u
n
Traducción a lógica clásica
T(w,p(t1,...,tn)) = p’(w,t1,...,tn)
n T(w,A) = T(w,A)
n T(w,AvB) = T(w,A) v T(w,B)
n T(w,xA) = xT(w,A)
n T(w,•A) = w’(R(w,w’) v
T(w’,A))
Teorema.
Sea L una logica multimodal.
n
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
n
n
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
n
n
n
n
n
n
n
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