Lógicas para aplicaciones software (página 2)

Partes: 1, 2

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: alpuente@dsic.upv.es
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