Lógica Temporal v701p

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’
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
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 rel="nofollow"> 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