Download 4. aplicaciones de la lógica temporal

Document related concepts

Lógica temporal wikipedia , lookup

Constante lógica wikipedia , lookup

Lógica modal wikipedia , lookup

Arthur Prior wikipedia , lookup

Lógica epistémica wikipedia , lookup

Transcript
LÓGICAS PARA LA
INFORMÁTICA Y LA
INTELIGENCIA ARTIFICIAL
Trabajo final 2006 – 2007
“Temporal Logic” de Antony Galton
Autor: Javier Pérez Rodríguez, 70886950 F
“Temporal Logic” por Antony Galton
Lógicas para la Informática y la Inteligencia Artificial
ÍNDICE DE CONTENIDOS
1. INTRODUCCIÓN ........................................................................................................ 3
2. APROXIMACIONES EN LÓGICA MODAL A LA LÓGICA TEMPORAL ........... 3
2.1. SEMÁNTICA EN LA LÓGICA TEMPORAL .................................................... 5
2.2. EXTENSIONES A LA LÓGICA TEMPORAL ................................................... 5
3. APROXIMACIONES EN LÓGICA DE PREDICADOS A LA LÓGICA
TEMPORAL..................................................................................................................... 6
3.1. ARGUMENTOS TEMPORALES ........................................................................ 6
3.2. “COSIFICACIÓN” DE ESTADO Y EVENTOS ................................................. 7
3.3. “COSIFICACIÓN” EVENTOS (EVENT-TOKEN) ............................................. 8
3.4. APROXIMACIONES HÍBRIDAS ....................................................................... 8
4. APLICACIONES DE LA LÓGICA TEMPORAL ...................................................... 8
Pérez Rodríguez, Javier
-2-
“Temporal Logic” por Antony Galton
Lógicas para la Informática y la Inteligencia Artificial
1. INTRODUCCIÓN
En este trabajo se pretende hacer una breve introducción a la lógica temporal, basándome en el artículo “Temporal Logic” escrito por Antony Galton para la Enciclopedia de
Filosofía de Stanford, e inicialmente publicado en Noviembre de 1999, y que actualmente se encuentra en la siguiente dirección: http://plato.stanford.edu/entries/logictemporal/#1 .
El término Lógica Temporal ha sido ampliamente utilizado para referirse a las distintas
aproximaciones a la representación de la información relativa al tiempo dentro del marco de trabajo de la lógica, y más especialmente para hablar de la propuesta introducida
por Arthur Prior en 1960, bajo el nombre de Tense Logic, ciertamente relacionada con
otras variedades de la lógica como es la lógica modal.
Por lo tanto, se emplea el término lógica temporal para referirse a un conjunto de simbolismos y reglas para la representación y el razonamiento sobre proposiciones en las que
está presente el tiempo. Se podría pensar en la sentencia “Tengo sueño”, y aunque en su
significado no interviene el tiempo, la verdad o falsedad de la misma puede variar con el
tiempo en un determinado sistema que incluya, por ejemplo, acciones de dormir. Por
ello, será cierta o falsa en función del sistema que se considere.
Algunas de sus posibles aplicaciones son su uso como marco de trabajo para definir la
semántica temporal de las expresiones en lenguaje natural, como lenguaje para reflejar
el conocimiento temporal en el contexto de la Inteligencia Artificial, y como herramienta para manejar aspectos temporales de la ejecución de programas informáticos. Así
pues, la lógica temporal está íntimamente relacionada con ciertas facetas de la ingeniería informática.
2. APROXIMACIONES EN LÓGICA MODAL A LA LÓGICA
TEMPORAL
El término de Tense Logic surge a raíz del interés de Arthur Prior por los estudios del
filósofo Diodoro Cronos (340-280 AC), aunque también se reconocen a Aristóteles ciertos escritos en los que aparecen expresiones semejantes a una lógica temporal de primer
orden.
El lenguaje de la lógica temporal contiene, además de los operadores tradicionales, otros
cuatro operadores modales cuyo significado se explica a continuación:
Operador
P
F
H
G
Significado
“En cierto tiempo se ha dado el caso de que...”
“En cierto tiempo se dará el caso de que...”
“Siempre se ha dado el caso de que...”
“Siempre se dará el caso de que...”
Pérez Rodríguez, Javier
-3-
“Temporal Logic” por Antony Galton
Lógicas para la Informática y la Inteligencia Artificial
Los operadores se pueden dividir en dos grupos: los dos primeros, P y F, son conocidos
como operadores temporales débiles, mientras que a los dos últimos, H y G, se les conoce como operadores temporales fuertes. No obstante, existen equivalencias entre los
dos grupos de operadores:
Pp ≡ ¬H¬p
“En cierto tiempo se ha dado p es equivalente a decir que es falso que siempre se
ha dado no p (es decir, es falso que nunca se ha dado p)”
Fp ≡ ¬G¬p
“En cierto tiempo se dará p es equivalente a decir que es falso que siempre se
dará no p”
En sus trabajos, Prior utilizó estos operadores para construir distintas fórmulas en las
que pretendía expresar algunas de las tesis filosóficas acerca del tiempo, y que podían
ser tomadas como axiomas de un sistema formal.
Uno de estos sistemas, que tiene especial importancia, es lo que se conoce como la Lógica Temporal Mímima Kt, que es generada por los siguientes cuatro axiomas:
p→HFp
p→GPp
H(p→q)→(Hp→Hq)
G(p→q)→(Gp→Gq)
junto con las dos reglas de inferencia temporal:
RH: probando p, entonces puedo probar Hp
RG: probando p, entonces puede probar Gp
y por supuesto las reglas de la lógica proposicional. Los teoremas de Kt vienen a expresar principalmente aquellas propiedades de los operadores temporales que no dependen
de ninguna suposición sobre el orden temporal. Más adelante se aclarará más este concepto.
Las lógicas temporales se obtienen añadiendo los operadores temporales a lógicas ya
existentes. Resulta de especial interés la lógica de predicados temporal, que se obtiene
añadiendo los operadores temporales a los clásicos predicados de primer orden, lo cual
nos permitirá expresar importantes distinciones entre la lógica del tiempo y la existencia.
Veamos un ejemplo de lógica proposicional temporal. Considerando la afirmación “Un
ministro será presidente del gobierno” podremos interpretarlas de diferentes maneras:
Pérez Rodríguez, Javier
-4-
“Temporal Logic” por Antony Galton
Lógicas para la Informática y la Inteligencia Artificial
 x(Ministro(x) & F Presidente(x))
 xF(Ministro(x) & Presidente(x))
F  x(Ministro(x) & F Presidente(x))
F  x(Ministro(x) & Presidente(x))
Alguien que actualmente es ministro llegará a
ser presidente en un tiempo futuro
Ahora existe alguien que será en un futuro ministro y presidente a la vez
Existirá alguien que sea ministro, y que después
será presidente
Existirá alguien que sea al mismo tiempo ministro y presidente a la vez
Se observa que la interpretación de cada fórmula puede ser problemática, ya que para
algunas, para poder interpretarlas correctamente será necesario introducir un dominio de
cuantificación que sea relativo al tiempo. Es decir, semánticamente será preciso añadir
un dominio de cuantificación D(t) para cada tiempo t. Eso nos lleva a plantear la semántica en la lógica temporal.
2.1. SEMÁNTICA EN LA LÓGICA TEMPORAL
Un concepto fundamental va a ser el de marco temporal, que es un conjunto T de entidades llamadas tiempos junto con una relación de orden < sobre T. Esto nos permite
definir un flujo de tiempo sobre el que definir el significado de los operadores lógicos.
De esta forma podremos dar un valor de verdad a cada formula en cada tiempo del marco temporal.
El significado de los operadores temporales sería el siguiente:




Pp es verdadero si y sólo si p es verdadero en un instante de tiempo t’ tal que t’<t
Fp es verdadero si y sólo si p es verdadero en un instante de tiempo t’ tal que t<t’
Hp es verdadero si y sólo si p es verdadero para todos los tiempos t’ tales que t’<t
Gp es verdadero si y sólo si p es verdadero para todos los tiempos t’ tales que t<t’
Ahora podremos precisar más sobre las características del sistema Kt o lógica mínima
temporal. Los teoremas de Kt serán precisamente aquellas fórmulas que son verdaderas
en cualquier tiempo bajo todas las interpretaciones sobre todos los marcos temporales.
2.2. EXTENSIONES A LA LÓGICA TEMPORAL
Aparte de los operadores PFHG ya comentados, en 1968 Kamp introdujo los operadores
S (since, desde) y U (until, hasta) cuyo significado es el siguiente:
Pérez Rodríguez, Javier
-5-
“Temporal Logic” por Antony Galton
Lógicas para la Informática y la Inteligencia Artificial
Operador Significado
Spq
“q ha sido verdadero desde el momento en que p era verdadero”
Upq
“q será verdadero hasta el momento en que p sea verdadero”
También es posible definir los operadores P y F en términos de S y U:
Pp≡ Sp(p ¬p)
Fp≡ Up(p ¬p)
Estos dos operadores se muestran especialmente útiles para ordenaciones temporales
estrictamente lineales.
Otro operador que se añade a los básicos es el operador O o “siguiente-instante”, que
asume que la series temporales están formadas por una secuencia discreta de tiempos
atómicos. Así el significado de este operador es el siguiente:
Operador Significado
Op
“p es verdadero en el instante de tiempo inmediatamente posterior”
Del mismo modo que se define el operador O se podría definir uno análogo pero para
instantes anteriores de tiempo, pero dado carece de interés en las principales aplicaciones de la lógica temporal.
3. APROXIMACIONES EN LÓGICA DE PREDICADOS A LA LÓGICA TEMPORAL
3.1. ARGUMENTOS TEMPORALES
Con este método, la dimensión temporal se recoge indicando para cada proposición un
argumento extra que contienen información temporal. Por ejemplo:
Gana ( España, CopaDavis, 2004)
Indica que España gana la Copa Davis en el año 2004
Si además incluimos en el lenguaje de predicados de primer orden un predicado < que
denote la relación temporal antes que, y una constante ahora, que indique el instante
actual, entonces podremos simular los operadores temporales en términos de lógica de
predicados (p(t) representa el resultado de introducir el argumento temporal extra al
predicado p):
Pérez Rodríguez, Javier
-6-
“Temporal Logic” por Antony Galton
Lógicas para la Informática y la Inteligencia Artificial
Operador
Pp
Fp
Hp
Gp
Equivalencia
 t(t<ahora & p(t))
 t(ahora<t & p(t))
 t(ahora<t → p(t))
 t(t<ahora → p(t))
Cabe destacar que antes de la aparición de la lógica temporal, este método de los argumentos temporales era la forma empleada para añadir información temporal a las expresiones lógicas.
3.2. “COSIFICACIÓN” DE ESTADO Y EVENTOS
El método de los argumentos temporales tenía dificultades si se quería poder distinguir
en el modelo entre, por ejemplo, estados, eventos y procesos, situación frecuente en el
campo de la inteligencia artificial.
Será preciso distinguir entre estados y eventos. Las proposiciones que hacen referencia
a estados tienen una incidencia temporal homogénea. Considérese el ejemplo “Carlos
está en coma”. Si por ejemplo Carlos está en coma desde el lunes hasta el jueves, entonces está en coma desde el lunes hasta el martes, desde el martes hasta el miércoles,
desde el miércoles hasta el jueves. Es cierto para cualquier subintervalo.
Por el contrario, las proposiciones que referencian eventos tienen una incidencia temporal no homogénea. Por ejemplo, “Pedro corre una maratón”. Si Pedro estuvo corriendo
desde las 10 hasta las 11:30, no puedo decir que estuviese corriendo una maratón desde
las 10 hasta las 10:45, pues en ese intervalo estaba realizando parte de la maratón (ahora
ya no es cierto para cualquier subintervalo).
Este método de “cosificar” estados y eventos fue introducido por James Allen, y expresa
la incidencia temporal usado dos predicados relacionales: Mantiene (Holds) y Ocurre
(Occurs):
Mantiene(Coma(Carlos),(Lunes, Jueves))
Occurre(Correr(Pedro,Maratón),(10 pm,12 pm))
La homogeneidad y no homogeneidad se asegura por axiomas como:
 s,i,i′(Mantiene(s,i) & En(i′,i) → Mantiene(s,i′))
 e,i,i′(Ocurre(e,i) & En(i′,i) → ¬Ocurre(e,i′))
(s: estado, i,i’: intervalos, e: evento)
donde En expresa la relación entre intervalos.
Pérez Rodríguez, Javier
-7-
“Temporal Logic” por Antony Galton
Lógicas para la Informática y la Inteligencia Artificial
3.3. “COSIFICACIÓN” EVENTOS (EVENT-TOKEN)
Se trata de un método propuesto por Donald Davidson en 1967, y usado en el contexto
computacional del Cálculo de Eventos de Kowalski y Sergot (1986).
Se trata de que cada predicado de evento sea dotado con un argumento extra en el que
se pondrá una variable que es una ocurrencia particular con fecha. Veamos un ejemplo:
Luis y Carlos comieron en un chino el sábado
Por lo tanto, Luis comió con Carlos el sábado
Puesto en forma lógica, según este método, quedaría de la siguiente forma:
 e (Comer(Luis, Carlos, e) & Lugar(e, restauranteChino) & Tiempo(e, sábado))
Por lo tanto,  e (Comer(Luis, Carlos, e) & Tiempo(e, sábado))
3.4. APROXIMACIONES HÍBRIDAS
También existen aproximaciones híbridas a la lógica temporal que dan lugar a Lógicas
Temporales Híbridas, en las cuales, además de las proposiciones y operadores temporales, tendremos proposiciones que son ciertas en instantes únicos de tiempo.
4. APLICACIONES DE LA LÓGICA TEMPORAL

Aplicación en el lenguaje natural, en el análisis de los tiempos verbales en inglés
así como de expresiones temporales del leguaje. En este ámbito, se considera
que la función de cada tiempo verbal es especificar una relación entre el momento en que se habla, S, el tiempo de referencia, R, y el tiempo del evento, E. Así,
se puede distinguir por ejemplo entre el pasado simple: “Comí arroz”, en el que
R=E<S, y el presente perfecto “He comido arroz”, para el que E<R=S. No obstante, Prior demostró que esto no era válido para la totalidad de formas verbales
usadas cotidianamente en el inglés.

Aplicación en la inteligencia artificial. Principalmente se emplea la lógica temporal para el famoso problema de marco, o axioma de marco, que plantea la necesidad de un razonamiento automático que permita conocer o deducir no sólo
aquellas propiedades del mundo que cambian como resultado de las acciones
(que nos las proporcionan los axiomas de efecto), sino también aquellas que no
cambian.
Pérez Rodríguez, Javier
-8-
“Temporal Logic” por Antony Galton
Lógicas para la Informática y la Inteligencia Artificial
Por ejemplo, supongamos que estamos viendo la televisión. El hecho de subir el
volumen no implica que se cambie el canal que estuviésemos viendo.

Aplicación en la informática. El estilo modal de la lógica temporal ha encontrado gran variedad de aplicaciones en el campo de la informática, sobre todo en lo
relacionado con la especificación y verificación de programas, generalmente
concurrentes, en los que las operaciones sobre los datos se realizan por más de
un procesador operando en paralelo. Parece obvio pensar que, si se quiere asegurar un correcto funcionamiento del sistema paralelo será necesario especificar la
forma en que se relacionan los distintos procesadores, es decir, habrá que definir
un mecanismo de coordinación para las acciones llevadas a cabo en el sistema.
Dado que varios procesadores podrían acceder de forma simultanea a un mismo
conjunto de datos, será preciso definir una cierta relación temporal entre las distintas acciones, para asegurar la integridad de la información compartida.
Generalmente se distingue entre las propiedades de la forma lógica temporal Fp,
que asegura que se obtendrán una serie de estados deseables durante la computación, y las propiedades de la forma Gp, que aseguran que nunca se alcanzarán
estados indeseables.
Pérez Rodríguez, Javier
-9-