Download Logica temporal - Universidad Nacional de Colombia

Document related concepts

Lógica temporal wikipedia , lookup

Lógica modal wikipedia , lookup

Lógica proposicional wikipedia , lookup

Constante lógica wikipedia , lookup

Lógica epistémica wikipedia , lookup

Transcript
ANEXO C. LÓGICA TEMPORAL
La lógica de predicados y la clásica se hallan limitadas para expresar todo
razonamiento debido a la falta de temporalidad, pues se centra en sentencias y
proposiciones que son validas indefinidamente. No todas las proposiciones tienen
(ni deben) ser validas por siempre, ni desde siempre; debido a esto surge la
necesidad de incluir el tiempo. Es aquí donde surge la lógica temporal que busca
especificar, expresar y razonar en los comportamientos dinámicos1.
En la lógica clásica, una proposición es verdadera o falsa, por ejemplo: Todas las
mujeres son de Venus, Jorge está en el parque, I=1, María estudia sistemas; pero al
considerar oraciones: Esta lloviendo, El parque está lleno, I=1 y I=2; las respuestas
"verdadera” o “falsa" depende del momento (tiempo) y el espacio (sitio). Es decir,
son proposiciones en que los valores de verdad dependen de tiempo. Luego “en la
lógica temporal, la misma oración puede tener diferente valor de verdad a
diferentes tiempos, una oración verdadera en cierto momento del pasado puede no
ser verdadera ahora y una sentencia verdadera ahora puede no permanecer así en
el futuro”.
Particularmente, la proposición I=1 y I=2, es falsa en la lógica clásica, pero tal vez
es cierta dado que la variable es dependiente del tiempo y para ello se tendría que
usar una formula como:
∃t, t´ tal que [t ≤ t´] ∧ [(I(t)=1) ∧ I(t´)=2)]
Es decir, se está representando un comportamiento dinámico. Formalmente la lógica
temporal es una extensión del cálculo de predicados en que se incluyen operadores
lógicos, modales y dependientes del tiempo como (siempre), Ο (next) y ◊ (algunas
veces). La lógica temporal se deriva también de la lógica modal y fue introducida a
mediados del siglo XX por Arthur Prior2.
Es una rama de la lógica cuyo objetivo es describir y razonar cuantitativamente
acerca de cómo cambian los valores de verdad de las proposiciones con respecto al
1
La lógica temporal es utilizada en filosofía con el objetivo fundamental de analizar y clarificar
conceptos clave recurrentes en su historia; la mayor parte de ellos señalados por Aristóteles como, la
casualidad y la necesidad, entre otros. No hay una sola lógica temporal sino que existen muchas,
dependiendo de la concepción del tiempo que tengamos o que deseemos utilizar.
2
Lógica modal es la lógica de la posibilidad y la necesidad, La lógica modal considerada usa los
operadores modales y ◊ que son llamados respectivamente operador “modal universal” y operador
“modal existencia”. Esos operadores actúan sobre fórmulas de la lógica proposicional modificando su
significado en el sentido de posibilidad y necesidad.
Inteligencia artificial
tiempo.
La lógica temporal sirve para especificar (y verificar) como componentes,
protocolos, objetos, módulos, procedimientos y funciones se comportan con el paso
del tiempo. Las especificaciones son hechas (temporalmente) con afirmaciones que
hacen aciertos sobre propiedades y relaciones entre pasado, presente y futuro. Se
toma acá, la lógica temporal de manera general.
La lógica temporal se define como la formalización de enunciados que incluyan
precisiones acerca del tiempo en que tienen lugar. En la lógica clásica los
enunciados: “está lloviendo” y “lloverá” se formalizan o bien como proposiciones
completamente diferentes o como la misma proposición; la lógica temporal permite
formalizarlas como una misma acción en dos momentos diferentes de tiempo; es
decir, permite discriminar si un hecho tiene lugar en el presente, en el pasado o en el
futuro. Para lograr este objetivo es necesario introducir a nivel sintáctico, nuevos
operadores referidos a los momentos del tiempo.
Existen varios tipos de lógica temporal, una en la que se considera que solo existe un
espacio futuro de sucesos (el tiempo lineal), otra en la que se consideran muchos
tiempos futuros alternativos y otras que consideran diferentes aspectos: intervalos,
modos, lieneal, dinámicas, etc.
El problema a enfrentar no es sencillo, los beneficios y aplicaciones en pro y en
contra de la lógica clásica y no-clásica son abundantes y es mucho el conocimiento
que existe al respecto; para que sea apropiado su estudio debe ajustarse a un entorno
apropiado de características básicas implicadas.
La lógica temporal se viene aplicando en los programas de computador. Existen
lenguajes especializados para este fin, pero ello no es válido si no se define un
sistema lógico.
Existen formas diferentes para definir un sistema lógico3.
3
Algunos cambios que la lógica ha tenido se debe a los intereses, los cuales continúan cambiando.
Hoy día los usos de los sistemas lógicos llevan de manera natural a construir nuevos sistemas,
expandiendo así la noción de racionalidad. Esta expansión no es ilimitada aunque bien puede ser
infinita. Es decir, hay infinitas formas o tipos de ser lógico, y por ende puede haber infinitas formas o
tipos de ser racional. Pero también hay infinitas maneras de pensar y procesar información que no
pueden ser rescatadas por ningún sistema lógico sensato, infinitas maneras irreductiblemente
irracionales. El que haya un sin fin de formas sensatas no hace sensata a cualquier forma. No puede
haber teoría de la racionalidad sin una filosofía de la lógica. Ser "lógico" es un requisito para ser
"racional", pero el ser "racional" no lleva a ser "lógico". Ser lógico conlleva a muchos compromisos
epistémicos y demanda tanto conocimiento como habilidades y actitudes. En su dimensión social,
exige saber cuándo es adecuado ofrecer razones, cómo contruirlas, cómo evaluarlas, cómo organizar
una discusión, apoyar con razones, aceptar consecuencias, saber cuándo y qué preguntar, clarificar el
discurso, tomar en cuenta el contexto de la discusión, reconocer la estructura de un argumento, saber
274 Luis Carlos Torres Soler
Lógica temporal
a. Sistemas lógicos como consecuencia de relaciones
Tradicionalmente para representar una lógica L, se requiere un alfabeto, un conjunto
de formulas y definir formalmente las consecuencias para esas formulas: dado ∆ y
una formula Q, se define la relación consecuente.
∆ |~L Q (Q sigue a ∆ en la lógica L)
La consecuencia de la relación es requerida para satisfacer las propiedades:
Reflexividad:
•
∆ |~ Q si Q ∈ ∆
Monotonicidad:
•
∆ |~ Q, ∆ ≡ ∆’ ,╠ ∆’ |~ Q
Transitividad (cut):
•
∆ |~ A; A |~ Q implica ∆ |~ Q
∆ es una base de datos y Q una petición. La reflexividad significa que la respuesta es
SI para cualquier Q que este en la base de datos. La monotonicidad refleja la
acumulación de datos, y la transitividad se refiere a que si ∆ |~ A, entonces A puede
ser usada para obtener Q desde ∆.
b Sistemas lógicos como prueba de algorítmica de sistemas
La importancia relativa de la deducción automatizada es en el incremento. En
general, una gran cantidad de conocimiento acerca de los sistemas lógicos surgen a
causa de su valor en ciencias de la computación, en especial la inteligencia artificial.
Los programas y los sistemas que se construyen debe poseer un sistema lógico, o
por lo menos, desarrolado dentro de alguno.
En muchos casos las bases de datos no solo contienen formulas de un tipo, sino que
tienen varios y no solo eso sino también son estructuradas. Muchos sistemas
algorítmicos se usan debido a esa estructura. Las características más importantes
son:
Las bases de datos se estructuran. No deben ser solamente conjunto de
•
formulas sino que deben tener una estructura.
Existe una relación debida a la estructuración, esta relación es: ∆ |~ A que es
•
la relación entre las bases de datos estructuradas ∆ y las formulas A.
cuando la evidencia es insuficiente y buscar alternativas. En muchos casoso la lógica ha sido
malentendida y quizá por ello existen detractores y malas enseñanzas. En nuestros días la lógica
informal en sus varias vertientes acude muy poco al simbolismo y la formalización; en algunos medios
se habla de aprendizaje "significativo", pero a veces el sentido significativo se asocia con aprender
jugando y cuyo contenido no debe ser abstracto y lograrse con mínima disciplina; y el desencanto y
escepticismo posmodernos excluye a la lógica. El aprendizaje de la lógica no es fácil, pero sí
constituye una base fuerte para el desarrollo del pensamiento creativo, sistémico, complejo, abstracto,
y todos los nombres generados por las diferentes corrientes de la filosofía, la educación y, en general,
las ciencias.
Universidad Nacional de Colombia
275
Inteligencia artificial
•
~ Debe satisfacer las condiciones de Identidad y Corte quirúrgico (surgical
cut).
c. Sistemas lógicos como un sistema de etiquetas deductivas
Un sistema lógico deductivo LDS (labelled deductive system) tiene su parte lógica
L, su parte algebraica (de operaciones) A y una disciplina de “etiquetar las formulas
de la lógica” M.
La forma de aplicar estas etiquetas es a partir de reglas deductivas, la forma de estas
reglas es más o menos uniforme para diferentes sistemas.
Para definir un sistema LDS lo que se hace es definir tanto su conjunto de formulas
como el conjunto de etiquetas.
Para este sistema se deben tener en cuenta los siguientes conceptos:
Una etiqueta atómica es cualquier t ∈ p. Una etiqueta es cualquier termino
•
generado por las funciones de símbolo f1,…, fm.
Una formula es cualquier formula de L.
•
Una unidad declarativa es un pareja (t, p), donde t es una etiqueta y p es una
•
formula.
Una base de datos es una unidad declarativa.
•
d) Sistemas agregados
En muchos casos se tienen sistemas que dan respuestas que parecen tener sentido,
las cuales pueden ser adecuadas y aplicadas, pero que no tuvieron un procedimiento
reconocido o comprendido por alguna lógica tradicional. El espíritu de este tipo de
sistemas es: Tres rumores son mejores que una prueba; Se hace desde siempre así
que vale.
Lenguajes temporales de primer orden y sus semánticas
Para llegar a entender con mayor claridad la lógica temporal es de especial interés
abordar este tema ya que nos permite expresar importantes distinciones respecto a la
lógica temporal y la existencia. Veamos esto con la ayuda de un ejemplo: Vamos a
tomar la frase Un filósofo será rey, esta frase puede ser interpretada de diferentes
maneras.
∃x(Filosofo(x) & F Rey(x)). Alguien que ahora es Filosofo será rey en algún
tiempo futuro.
b) ∃xF (Filosofo(x) & Rey(x)). Ahora existe un alguien que en el futuro será
Filosofo y rey.
c) F∃x (Filosofo(x) & F Rey(x)). Va existir alguien que será Filosofo y después
será rey.
d) F∃x(Filosofo(x) & Rey(x)). Existirá alguien que será Filosofo y rey al mismo
a)
276
Luis Carlos Torres Soler
Lógica temporal
tiempo.
El lenguaje LTp de lógica temporal
El punto a considerar son los diferentes puntos de tiempo que generan diferentes
valores de verdad en las proposiciones y que permiten hacer un primer acuerdo
importante: asumimos que el juego de puntos de tiempo es infinito, discreto y
linealmente ordenado con el elemento más pequeño.
Ahora si consideramos una proposición cualquiera p. Para poder describir la posible
variedad de los valores de verdad de p a diferentes tiempos t el más simple de los
medios de la lingüística sería introducir un parámetro de tiempo explicito en la
proposición y denotado por p(t). Es de preferencia tener operadores lógicos
manuales que permitan formular nuevas proposiciones. Sin necesidad de cambiar los
parámetros de las proposiciones.
El lenguaje de la lógica temporal usa los mismos símbolos y reglas establecidas para
la lógica clásica de predicados; También es un modelo encerrado en la lógica modal.
Un frame temporal consiste en conjunto T de entidades denominadas “tiempos”
junto con una relación que orden < sobre t. Esto define un flujo del tiempo sobre el
cual los operadores temporales son definidos. Sin embargo, en la lógica temporal
Prior estableció cuatro operadores monarios (G, H, F y P).
G: “Será siempre en el futuro verdad”
H: “Ha sido siempre en el pasado verdad”
F: “Será alguna vez en el futuro verdad”
P: “Fue alguna vez en el pasado verdad”
G y F se conocen como operadores de tiempo débiles mientras que H y P son
conocidos como operadores de tiempo fuertes. Estos pares pueden ser generalmente
abordados como ínterdefinibles por equivalencias:
Pp ≡ -H-p
y
Fp ≡ -G-p
Para dar una interpretación podemos, por ejemplo, definir los operadores temporales
débiles usando algunas reglas:
a. Pp es verdad en t si y solo si p es verdad en algún tiempo t’ tal que t’< t.
b. Fp es verdad en t si y solo si p es verdad en algún tiempo t’ tal que t< t’.
Para los operadores fuertes:
a. Hp es verdad en t si y solo si p es verdad en todo t’ tal que t’<t.
b. Gp es verdad en t si y solo si p es verdad en todo t’ tal que t< t’.
Prior utilizó los operadores para construir expresiones sobre el tiempo las cuales
Universidad Nacional de Colombia
277
Inteligencia artificial
pueden ser tomadas como axiomas si se desea4.
a) GpÆFp “Lo que siempre será, será”
b) G(pÆq) Æ(GpÆGq) “Si p siempre implica a q, entonces si p es siempre, q
también”.
Al introducir en el lenguaje de primer orden el símbolo < que denote la relación de
orden temporal “Antes que” y la constante “ahora” que denote el tiempo presente;
de esta manera los operadores temporales pueden ser interpretados de la siguiente
manera:
Pp ≡ ∃t (t<ahora & p(t))
Fp ≡ ∃t (ahora<t & p(t))
Gp ≡ ∀t (t<ahora → p(t))
Hp ≡ ∀t (ahora<t → p(t))
Donde p(t) representa el resultado de introducir un argumento temporal que implica
las variables del predicado que ocurren en p. Esto se llama método de argumentos
temporales5.
Sistema mínimo de lógica temporal, Kt
Este sistema esta compuesto por los siguientes cuatro axiomas y dos reglas de
inferencia temporal.
Axiomas
Ax1. G (p→q) → (Gp→Gq)
Ax2. H (p→q) → (Hp→Hq)
Ax3. p → HFp
Ax4. p → GPp
Reglas de inferencia temporal
RH: De una prueba de p, deriva la prueba para Hp.
RG: De una prueba de p, deriva la prueba para Gp.
Si al sistema mínimo de lógica temporal se agregan los axiomas:
4
Para el año de 1967 Prior reporto un trabajo bastante extenso sobre lógica temporal postulando
diversas y diferentes combinaciones de axiomas. Es sin duda A. Prior el más grande constructor de
lógicas temporales y a él cabe adjudicar el título de fundador de ese tipo de lógica. Sin embargo, la
lógica temporal difiere en un punto central del género de lógicas desarrolladas por Prior y otros:
éstas últimas son lógicas del tiempo verbal, tense logics. Las lógicas del tiempo verbal introducen
primitivos operadores que significan `Es pasado que' o `Es futuro que', o sus parónimos. Una lógica
cronológica acude a un procedimiento totalmente diverso: en vez de asignar a los estados de cosas
determinaciones absolutas de ser pasado o futuro, introduce relaciones temporales primitivas y
también una cuantificación sobre «cuándo».
5
Antes de la incursión de la lógica temporal el método de los argumentos temporales era una de las
opciones mas usadas dentro de los formalismos para expresiones lógicas con información temporal.
278 Luis Carlos Torres Soler
Lógica temporal
Ax5. PPp → Pp
Ax6. FFp → Fp
Se tendrá modelos transitivos.
Y si además se añaden los axiomas:
Ax7. PFp → (Pp v p v Fp)
Ax8. FPp → (Pp v p v Fp)
Se tendrá sistemas para el tiempo lineal.
Aproximación de la lógica de predicados a la lógica temporal
Las proposiciones que representan estados tales como "Maria está dormida" tienen
incidencia temporal homogénea, estas se deben sostener en un conjunto de
subintervalos contenidos en un intervalo (si Maria está dormida a partir de la 1 a las
6 entonces ella está dormida entre la 1 y las 2, las 2 a las 3, etc.). Por el contrario, las
proposiciones que representan acontecimientos (tales como "Luis camina al parque")
tienen incidencia temporal no homogénea; esto implica que la proposición no es
verdad en ninguno de los subintervalos de un intervalo del cual sea verdad. Para
comprender esto analicemos un poco mejor la situación. Si Luis camina al parque en
el intervalo entre 1:00 y 1:15, entonces no es el caso que él camina al parque en el
intervalo de 1:00 a 1:05 pues en este intervalo él camina parte del camino a la
estación.
Veamos la notación para nuestros dos ejemplos:
mantiene (dormida(Maria), (1:00 am, 6:00 am))
ocurre (camina a(Juan), (1:00 pm,1:15 pm))
Aquí se ve expresada de una manera muy obvia la notación (t, t’)
Este método fue introducido para suplir las necesidades respecto a casos como los
nombrados anteriormente, este método esta asociado al nombre de James Allen.
Lógica del tiempo indeterminista
El término tiempo indeterminista se refiere a que los acontecimientos suceden en el
tiempo de manera indeterminada, es decir, el futuro esta indeterminado, es abierto y
lleno de posibilidades. Dentro de la lógica temporal esta afirmación acerca del
tiempo a llevado al siguiente interrogante: Una vez que un suceso se convierte en
pasado, ¿hubiese sido verdad afirmar que iba a suceder? Este tema es tratado por las
corrientes Ockhamista y Peirceana.
La Ockhamista se inclina por decir que basta que un suceso acontezca en el futuro
para afirmar que fue verdadera la afirmación en el pasado de que iba a suceder; la
segunda, la Peirceana, prefiere afirmar que para que un suceso se de en el futuro no
Universidad Nacional de Colombia
279
Inteligencia artificial
implica que fuese verdad en el pasado que éste iba a suceder, sólo se puede hablar
de la verdad de un enunciado acerca del futuro si éste es inevitable.
Por ejemplo: Si un bebé está próximo a nacer y se hace alguna afirmación acerca del
sexo que tendrá el bebé, para la visión Ockhamista, que una afirmación hecha en el
pasado sea verdadera es que en el futuro la aseveración se cumpla; es decir, si se dijo
que era niña y nace niña la aseveración hecha antes del nacimiento fue verdadera.
Para la visión Peirceana, la única manera que la aseveración fuera cierta sería
diciendo el bebé nacerá niño o niña, es decir tomando todas las posibilidades de tal
forma que no haya manera de equivocarse.
Arthur Prior, quien inició fructíferamente varias líneas de trabajo en lógica temporal,
es el primero en plantearse la construcción de una lógica del tiempo indeterminista
(también llamada lógica de la necesidad histórica)6. Lo que Prior plantea es la
construcción de una lógica que refleje que los sucesos futuros son realmente
contingentes, mientras que los hechos pasados, históricos, son ya inevitables y, por
tanto, necesarios.
La lógica temporal introduce los operadores modales al tener en cuenta que el
tiempo puede representarse como una línea recta en la cual a partir de un punto se
abren varias bifurcaciones, la línea representaría el pasado, el punto el presente y las
bifurcaciones las posibilidades en el futuro; de esta manera si dentro de una de esas
posibilidades del futuro se da el suceso x, afirmar “Es posible en el futuro x” es
verdadero, si el suceso se da en todas las bifurcaciones, es decir en todas las
posibilidades futuras entonces x es históricamente necesaria y afirmar “Es necesario
en el futuro x” es verdadero.
De manera simplificada podrían tomarse las axiomatizaciones de la lógica temporal
hechos anteriormente y agregarle los siguientes axiomas:
•
•
•
p → Lp, para toda p que no contenga a F. (necesidad histórica)
(¬q ^ Hq ^ Lp) → GLH((¬q ^ Hq) →p)
p →GLPp
Como se dijo anteriormente, la lógica temporal también se desarrolla desde sus
bases proposicionales de lógica de predicados de primer orden.
Sea LP un lenguaje clásico de primer orden. Un lenguaje temporal de primer orden
LTp es una extensión de LP donde: LTp contiene todo LP adicionando los símbolos □,
6
. El desarrollo de la lógica del tiempo indeterminista es bastante reciente y se ha intensificado
especialmente en estos últimos años, debido en parte a la utilidad de las mismas en el campo de la
informática, por lo que muchos de los desarrollos son provisionales y algunos, como es el caso de
alguna axiomatización, permanecen todavía como problemas abiertos..
280 Luis Carlos Torres Soler
Lógica temporal
Ο y atnext (esto es: incluyendo el tiempo). Además, el conjunto de variables son
particionadas en dos subgrupos llamados el conjunto de variables globales y locales
respectivamente. Los términos y las formulas atómicas son definidas como en LP.
Ejemplos de operadores desiderables con sus respectivos significados informales:
•
•
•
•
•
Οp: "una espera en el tiempo inmediatamente después del punto de
referencia”
□p: "una espera en todos los tiempos después del punto de referencia"
◊p: "hay un tiempo después del punto de referencia que tiene una espera"
p atnext q: "una futura espera al próximo punto de tiempo donde q espera".
p until q: "una espera en todos los tiempos siguientes a un punto de tiempo
en el que q espera"
Así pues un lenguaje LTp de la lógica temporal proposicional esta dado por lo
siguiente:
Alfabeto
Un conjunto enumerable ν de formulas bien formadas
Los símbolos ⌐, →, Ο, □, atnext, ‘(‘, ‘)’.
Definición inductiva de formulas
Cada formula atómica es una fórmula.
•
Si p es una formula entonces también ⌐p, Οp y □p son fórmulas.
•
Si p y q son formulas entonces (p → q) y (p atnext q) son fórmulas.
•
Si p es una formula y x es una variable global entonces ∀ x p(x) es una
•
fórmula.
Semántica de LTp
La semántica del LTp esta dada al extender la noción de estructura temporal.
Una estructura temporal (de primer orden) K =(S,ξ,W) para LTp consiste en:
™ Una estructura S para el kernel LP del LTp
™ Una valoración de la variable global ξ respecto a S.
™ Una secuencia infinita W = {η0, η1, η2,…} de estados donde cada ηi es una
valoración de la variable global respecto a S.
Ahora definamos inductivamente el conjunto de Ki(F) ∈{f, t} para cada K=(S, ξ, W)
(ξ η
1. Ki(p) = S , i) (p)
2. Ki(⌐p) = t
3. Ki(p → q) = t
4. Ki(Οp) = t
para toda fórmula atómica.
iff Ki (p) = f
iff Ki (p) = f
or Ki(q)=t
iff Ki+1(p) = t
Universidad Nacional de Colombia
281
5. Ki(□p) = t
6. Ki(p atnext q) = t
7. Ki( ∀ x p) = t
Inteligencia artificial
iff Kj(p) = t
para todo j ≥ i
iff Kj(q) = f
para todo j > i or
Kk(p) = t
para el mas pequeño valor de k>i
con Kk(q) = t
iff K´i(q) = f
para cada estructura temporal
ξ´,W))
=
ξ´(y)
= ξ(y) para cada y.
K´(S,
t
Leyes de la lógica temporal
En cualquier lógica, las fórmulas válidas expresan las “leyes lógicas”. Por ejemplo,
la ley de DeMorgan:
⌐(p ∩ q)
↔
(p U ⌐q)
(1).
Acorde a las definiciones semánticas es de esperarse que las tautologías
permanezcan válidas en la lógica temporal donde podemos sustituir formulas de LTp
para p y q, así la ley de DeMorgan quedaría de la siguiente manera:
⌐(Οp ∩ □q)
↔
(⌐Οp U ⌐□q)
(2).
El conjunto de fórmulas que representan las leyes de la lógica temporal serían:
Leyes de dualidad:
1) ⌐Οp
2) ⌐□p
3) ⌐◊p
↔
↔
↔
Ο⌐p
◊⌐p
□⌐p
Leyes de reflexividad:
4) □p → p
5) p → ◊p
Leyes de idempotencia:
↔
6) □□p
↔
7) ◊◊p
□p
◊p
Leyes distributivas:
8) Ο(p → q)
9) Ο(p ∩ q)
10) Ο(p U q)
11) Ο(p atnext q)
12) □(p ∩ q)
13) ◊(p U q)
14) (p ∩ q) atnext k
15) (p U q) atnext k
↔
↔
↔
↔
↔
↔
↔
↔
1) Leyes commutativas
282
Luis Carlos Torres Soler
Οp → Οq
Οp ∩ Οq
Οp U Οq
Οp atnext Οq
□p ∩ □q
◊p U ◊q
p atnext k ∩ q atnext k
p atnext k U q atnext k
Lógica temporal
16) □Οp ↔ Ο□p
17) ◊□p ↔ □◊p
2) Leyes de generalización temporal
18) p ╟ q ↔ □p → q
19) □p → q ╟ □p → □q
20) p → ◊q ╟ ◊p → ◊q
Extensiones de la lógica temporal
Después de la introducción de la sintaxis básica (PFGH) esta se ha ido expandiendo
de varias maneras hasta el día de hoy.
Operadores binarios temporales. Los operadores binarios temporales S y U (Since y
Until del ingles “desde” y “hasta”) fueron introducido en el año de 1968.
Spq:: q ha sido verdad desde un tiempo en el que p fue verdad.
Upq:: q será verdad hasta el tiempo en el que p sea verdad.
Igualmente se definen algunos operadores monarios, mencionados anteriormente, en
término de S y U de la siguiente manera:
Pp ≡ Sp(p v ¬p)
Fp ≡ Up(p v ¬p)
La importancia de estas relaciones radica en que se expresan completamente
respecto a las propiedades temporales de primer orden, estrictamente las órdenes
lineales temporales.
Lógica métrica temporal. Prior introdujo la nomenclatura Fnp para representar “Será
alguna vez en el futuro n, por lo tanto será p”. No se necesita una notación separada
para Fnp al poderse escribir F(-n)p para “Fue alguna vez en el pasado n así que p
fue”.
Podemos definir los operadores no métricos de la siguiente manera:
Pp ≡ ∃n(n<0&Fnp)
Fp ≡ ∃n(n>0&Fnp)
Hp ≡ ∀n(n<0ÆFnp)
Gp ≡ ∀n(n>0ÆFnp)
El operador ”próxima vez" Ο. Este operador asume que las series de tiempo son una
secuencia discreta de tiempos. De esta manera, el operador Op nos dice que “p es
verdad en el instante inmediatamente posterior de un paso (señal discreta). Con el
tiempo discreto podemos definir Op en términos del operador U “until”: Op ≡
Up(p&-p).
Esto implica que “p será verdad en algún tiempo futuro; sin embargo, entre el
presente y ese tiempo futuro nada es verdad.
Universidad Nacional de Colombia
283
Inteligencia artificial
En el tiempo discreto el operador de tiempo futuro esta relacionado con el operador
“próxima vez” de la siguiente manera:
Fp ≡ Op v OFp.
Anteriormente hemos mencionado un operador temporal razonable que no ha sido
considerado formalmente:
(p until q).
También se encuentran operadores razonables adicionales que podrían ser útiles para
las aplicaciones particulares.
•
•
•
p unless q: “Si hay un punto de tiempo siguiente al que q espera entonces p
para en ese punto o sino p espera permanentemente”.
p while q: “p espera mientras que q espere(en el futuro)”.
p before q: “Si q espera algunas veces en el futuro entonces p también espera
antes de eso”
Los operadores ◊, □, Ο pueden ser expresados por el operador atnext , de igual
forma se escriben en términos de los operadores until, unless, while y before:
↔
1) p until q
q atnext (p → q) ∩ Ο◊q
2) p unless q ↔
q atnext (p → q)
↔
⌐q atnext (p → ⌐q)
3) p while q
⌐q atnext (p U q)
4) p before q ↔
El sistema formal ∑Tp
Después de la definición semántica de formulas validas de la lógica temporal
proposicional, se tiene un sistema formal ∑Tp para la derivación formal de algunas
formulas, axiomas y reglas generales:
Axiomas:
(taut) “todas las formulas derivadas son tautológicamente validas”.
↔
1) ⌐Οp
Ο⌐p
→q)
↔
2) Ο (p
(Οp → Οq)
3) □p → p ∩ Ο□p
4) Ο □⌐p → (p atnext q)
5) (p atnext q → Ο (q → p) ∩ Ο (⌐q → p atnext q)
6) ∀ x p → px(t) si t es sustituible por x en p,
7) ∀ x Οp → Ο ∀ xp.
8) p → Οp si p no contiene variables locales.
(eq1) x = x;
284
Luis Carlos Torres Soler
Lógica temporal
(eq2) x = y → (p → px(y)) si p no contiene operadores temporales.
Reglas:
(mp) p, p → q├ q,
(nex) p├ Οp,
(ind) p → q, p → Οp├ p → □q.
(gen) p→ q├ p→ ∀ xq. si no hay libre ocurrencia de x en p.
No estamos interesados en determinar como las tautologías clásicas pueden
derivarse de algunos axiomas, simplemente tomamos todos ellos como axiomas. La
regla (ind) es una regla de inducción que significa:
“Si p (siempre) implica q y p es invariante de tiempo cualquiera al siguiente
entonces p implica q siempre”.
Esto nos permite derivar sólo fórmulas que son válidas en todo ∑Tp.
Principios de inducción
En el sistema formal ∑Tp, cada fórmula valida puede ser derivada. Ahora veremos
algunos principios o estrategias para derivar algún tipo especial de formulas como la
que tenemos a continuación:
p → □q.
La regla (ind):
p → q, p → Οq├ p → □q.
Que está contenida en ∑Tp, la cual a su vez es un principio general de inducción para
proveer p → □q; más precisamente es un principio de inducción que para estar
seguro que p → □q, debemos verificar si p → q y si es invariante en cualquier
estado de transición. Primero tenemos que formular dos variantes de (ind) que sean
mas útiles para aplicaciones subsecuenciales, así pues:
(ind´) p → Οp├ p → □p.
(ind´´) p → q, q → Οq├ p → □q.
Derivación de (ind´)
1
p → Οp
2
p → p (taut)
3
p→ □p (ind), (1), (2).
Derivación de (ind´´)
1
p → q.
2
q → Οq
3
q → □q (ind´), (2)
Universidad Nacional de Colombia
285
4
Inteligencia artificial
p → □q (prop), (1), (3).
De todo se puede concluir:
↔
i) ∀xΟp
↔
ii) ∃ xΟp
↔
iii) ∀x□p
◊Ap
↔
iv) ∃ x
v) ∀ x(p atnext q)
vi) ∀ x(p atnext q)
Ο∀xp
Ο ∃ xp
□∀xp
◊ ∃ xp
↔ ∀xp (atnext q) si no hay libre ocurrencia de x en q.
↔ ∀ xp (atnext q) si no hay libre ocurrencia de x en q.
Resumen
El tiempo es un factor predominante en la vida diaria, y así debe ser también para
los modelos de sistemas que se desarrollan. La lógica temporal es una forma de
incluir el tiempo. De cierta manera la única forma de lograr una verdadera
representación de la realidad y llegar a una verdadera inteligencia artificial es
incluyendo el criterio temporal de verdad.
Así que si se piensa en Inteligencia artificial, un paso lógico hacia su verdadera
consecución es el manejo adecuado del tiempo. Ninguna inteligencia es ajena al
tiempo. Este el que determina su prevalencia y la validez de sus conocimientos.
La lógica temporal permite formalizar una acción en momentos diferentes. Introduce
los operadores modales. No hay una sola lógica temporal sino que existen muchas,
dependiendo de la concepción del tiempo que se tenga o que se desea utilizar.
El término tiempo indeterminista se refiere a que el futuro esta indeterminado
abierto y lleno de posibilidades.
La lógica temporal, aunque sea de complicada representación, es un acercamiento
muy intuitivo a la forma de pensar de las personas, se aproxima a lo que se
denomina “pensar en el futuro” y en “recordar”, pues son estas dos definiciones las
que caracterizan la vida de una persona, la evaluación de hecho pasados y de hechos
futuros. Nadie piensa únicamente en el presente.
Bibliografía
BOOLOS George, Jeffrey Richard (1974). Computability and Logic. Cambridge
University Press, Cambridge: UK.
GABBAY Dov M., HOGGER C.J. (1994). Handbook of logic in artificial
intelligence and logic programing, Oxford.
286
Luis Carlos Torres Soler
Lógica temporal
GABBAY Dov M., REYNOLDS Mark A., FINQUER Marcelo (2000).
Mathematical Fundations and Computational Aspects. Vol. 2, Oxford University
Press, Oxford.
GALTON Anthony (1994). The Logic of Aspect. Clarendon Press, Oxford.
HUGHES George Edward, CRESSWELL M. J. (1973). Introducción a la lógica
modal. Tecnos, Madrid.
PRIOR Arthur N. (1976). Historia de la Lógica. Tecnos, Madrid.
QUINE W.V. (1960). Methods of Logic. Henry Hold, New York.
KRÔGER Fred (1987). Temporal Logic of Programs. Springer-Verlag, Berlin.
VAN BENTHEM J. (1991). The Logic of Time. 2ª ed., Kluwer Academic
Publishers, Boston.
Universidad Nacional de Colombia
287