stringtranslate.com

Lógica temporal

En lógica , la lógica temporal es cualquier sistema de reglas y simbolismo para representar y razonar proposiciones calificadas en términos de tiempo (por ejemplo, " siempre tengo hambre", " algún día tendré hambre" o "tendré hambre hasta que coma algo"). A veces también se usa para referirse a la lógica temporal , un sistema de lógica temporal basado en la lógica modal introducido por Arthur Prior a fines de la década de 1950, con importantes contribuciones de Hans Kamp . Ha sido desarrollado posteriormente por científicos informáticos , en particular Amir Pnueli , y lógicos .

La lógica temporal ha encontrado una aplicación importante en la verificación formal , donde se utiliza para indicar los requisitos de los sistemas de hardware o software. Por ejemplo, se puede decir que siempre que se realiza una solicitud, se concede el acceso a un recurso , pero nunca se concede a dos solicitantes simultáneamente. Tal afirmación se puede expresar convenientemente en una lógica temporal.

Motivación

Consideremos la afirmación "tengo hambre". Aunque su significado es constante en el tiempo, el valor de verdad de la afirmación puede variar con el tiempo. A veces es verdadera y a veces falsa, pero nunca simultáneamente verdadera y falsa. En una lógica temporal, una afirmación puede tener un valor de verdad que varía con el tiempo, en contraste con una lógica atemporal, que se aplica solo a afirmaciones cuyos valores de verdad son constantes en el tiempo. Este tratamiento del valor de verdad a lo largo del tiempo diferencia la lógica temporal de la lógica verbal computacional.

La lógica temporal siempre tiene la capacidad de razonar sobre una línea de tiempo. Las llamadas lógicas de "tiempo lineal" se limitan a este tipo de razonamiento. Las lógicas de tiempo ramificado, sin embargo, pueden razonar sobre múltiples líneas de tiempo. Esto permite, en particular, el tratamiento de entornos que pueden actuar de manera impredecible. Para continuar con el ejemplo, en una lógica de tiempo ramificado podemos afirmar que "existe la posibilidad de que siga teniendo hambre para siempre" y que "existe la posibilidad de que, con el tiempo, ya no tenga hambre". Si no sabemos si alguna vez seré alimentado o no, ambas afirmaciones pueden ser verdaderas.

Historia

Aunque la lógica de Aristóteles se centra casi exclusivamente en la teoría del silogismo categórico , hay pasajes en su obra que ahora se consideran anticipaciones de la lógica temporal y pueden implicar una forma temprana, parcialmente desarrollada, de lógica bivalente modal temporal de primer orden . Aristóteles estaba particularmente preocupado por el problema de los contingentes futuros , donde no podía aceptar que el principio de bivalencia se aplique a afirmaciones sobre eventos futuros, es decir, que podamos decidir en el presente si una afirmación sobre un evento futuro es verdadera o falsa, como "mañana habrá una batalla naval". [1]

Hubo poco desarrollo durante milenios, señaló Charles Sanders Peirce en el siglo XIX: [2]

Los lógicos han considerado habitualmente que el tiempo es lo que se denomina materia «extralógica». Yo nunca he compartido esta opinión, pero he pensado que la lógica no había alcanzado todavía el estado de desarrollo en el que la introducción de modificaciones temporales de sus formas no provocaría una gran confusión; y todavía soy muy partidario de esa manera de pensar.

Sorprendentemente para Peirce , el primer sistema de lógica temporal fue construido, hasta donde sabemos, en la primera mitad del siglo XX. Aunque Arthur Prior es ampliamente conocido como el fundador de la lógica temporal, la primera formalización de dicha lógica fue proporcionada en 1947 por el lógico polaco Jerzy Łoś . [3] En su obra Podstawy Analizy Metodologicznej Kanonów Milla ( Los fundamentos de un análisis metodológico de los métodos de Mill ) presentó una formalización de los cánones de Mill . En el enfoque de Łoś , se hizo hincapié en el factor tiempo. Por lo tanto, para alcanzar su objetivo, tuvo que crear una lógica que pudiera proporcionar medios para la formalización de las funciones temporales. La lógica podría verse como un subproducto del objetivo principal de Łoś , [4] aunque fue la primera lógica posicional que, como marco, se utilizó más tarde para las invenciones de Łoś en lógica epistémica . La lógica en sí tiene una sintaxis muy diferente a la lógica temporal de Prior, que utiliza operadores modales. El lenguaje de la lógica de Łoś utiliza más bien un operador de realización, propio de la lógica posicional, que vincula la expresión con el contexto específico en el que se considera su valor de verdad. En la obra de Łoś , este contexto considerado era solo temporal, por lo que las expresiones estaban vinculadas a momentos o intervalos de tiempo específicos.

En los años siguientes, Arthur Prior comenzó a investigar la lógica temporal . [4] Se interesó por las implicaciones filosóficas del libre albedrío y la predestinación . Según su esposa, consideró por primera vez formalizar la lógica temporal en 1953. Los resultados de su investigación se presentaron por primera vez en la conferencia en Wellington en 1954. [4] El sistema que presentó Prior era similar sintácticamente a la lógica de Łoś , aunque no fue hasta 1955 que se refirió explícitamente al trabajo de Łoś , en la última sección del Apéndice 1 de la Lógica formal de Prior . [4]

Prior dio conferencias sobre el tema en la Universidad de Oxford en 1955-6, y en 1957 publicó un libro, Tiempo y modalidad , en el que introdujo una lógica modal proposicional con dos conectivos temporales ( operadores modales ), F y P, correspondientes a "en algún momento en el futuro" y "en algún momento en el pasado". En este trabajo temprano, Prior consideró que el tiempo es lineal. Sin embargo, en 1958, recibió una carta de Saul Kripke , quien señaló que esta suposición quizás no esté justificada. En un desarrollo que prefiguró uno similar en la ciencia de la computación, Prior tomó esto en consideración y desarrolló dos teorías del tiempo ramificado, que llamó "Ockhamista" y "Peirceana". [2] [ aclaración necesaria ] Entre 1958 y 1965 Prior también se carteó con Charles Leonard Hamblin , y una serie de desarrollos tempranos en el campo se pueden rastrear a esta correspondencia, por ejemplo, las implicaciones de Hamblin. Prior publicó su obra más madura sobre el tema, el libro Pasado, presente y futuro, en 1967. Murió dos años después. [5]

Junto con la lógica temporal, Prior construyó algunos sistemas de lógica posicional, que heredaron sus ideas principales de Łoś . [6] El trabajo en lógicas temporales posicionales fue continuado por Nicholas Rescher en los años 60 y 70. En obras como Nota sobre lógica cronológica (1966), Sobre la lógica de proposiciones cronológicas (1968) , Lógica topológica (1968) y Lógica temporal (1971) investigó las conexiones entre los sistemas de Łoś y Prior . Además, demostró que los operadores temporales de Prior podían definirse utilizando un operador de realización en lógicas posicionales específicas. [6] Rescher , en su trabajo, también creó sistemas más generales de lógicas posicionales. Aunque los primeros se construyeron para usos puramente temporales, propuso el término lógicas topológicas para lógicas que estaban destinadas a contener un operador de realización pero no tenían axiomas temporales específicos, como el axioma del reloj.

Los operadores temporales binarios Since y Until fueron introducidos por Hans Kamp en su tesis doctoral de 1968, [7] que también contiene un resultado importante que relaciona la lógica temporal con la lógica de primer orden , un resultado ahora conocido como el teorema de Kamp. [8] [2] [9]

Dos de los primeros contendientes en las verificaciones formales fueron la lógica temporal lineal , una lógica de tiempo lineal de Amir Pnueli , y la lógica de árbol de cálculo (CTL), una lógica de tiempo de ramificación de Mordechai Ben-Ari , Zohar Manna y Amir Pnueli. Un formalismo casi equivalente a CTL fue sugerido por la misma época por EM Clarke y EA Emerson . El hecho de que la segunda lógica pueda ser decidida de manera más eficiente que la primera no se refleja en las lógicas de tiempo de ramificación y lineal en general, como a veces se ha argumentado. Más bien, Emerson y Lei muestran que cualquier lógica de tiempo lineal puede extenderse a una lógica de tiempo de ramificación que puede ser decidida con la misma complejidad.

La lógica posicional de Łoś

La lógica de Łoś fue publicada como su tesis de maestría de 1947 Podstawy Analizy Metodologicznej Kanonów Milla ( Los fundamentos de un análisis metodológico de los métodos de Mill ). [10] Sus conceptos filosóficos y formales podrían verse como continuaciones de los de la Escuela de Lógica de Lviv-Varsovia , ya que su supervisor fue Jerzy Słupecki , discípulo de Jan Łukasiewicz . El artículo no fue traducido al inglés hasta 1977, aunque Henryk Hiż presentó en 1951 una revisión breve, pero informativa, en el Journal of Symbolic Logic . Esta revisión contenía conceptos centrales del trabajo de Łoś y fue suficiente para popularizar sus resultados entre la comunidad lógica. El objetivo principal de este trabajo fue presentar los cánones de Mill en el marco de la lógica formal. Para lograr este objetivo, el autor investigó la importancia de las funciones temporales en la estructura del concepto de Mill. Con esto en mente, proporcionó su sistema axiomático de lógica que serviría como marco para los cánones de Mill junto con sus aspectos temporales.

Sintaxis

El lenguaje de la lógica publicada por primera vez en Podstawy Analizy Metodologicznej Kanonów Milla ( Los fundamentos de un análisis metodológico de los métodos de Mill ) consistía en: [3]

El conjunto de términos (denotado por S) se construye de la siguiente manera:

El conjunto de fórmulas (denotado por For) se construye de la siguiente manera: [10]

Sistema axiomático original

Lógica temporal de Prior (LT)

La lógica del tiempo oracional introducida en Tiempo y Modalidad tiene cuatro operadores modales (no funcionales a la verdad ) (además de todos los operadores funcionales a la verdad habituales en la lógica proposicional de primer orden ). [11]

Estos se pueden combinar si dejamos que π sea un camino infinito: [12]

A partir de P y F se pueden definir G y H , y viceversa:

Sintaxis y semántica

Una sintaxis mínima para TL se especifica con la siguiente gramática BNF :

donde a es alguna fórmula atómica . [13]

Los modelos de Kripke se utilizan para evaluar la verdad de las oraciones en TL. Un par ( T , <) de un conjunto T y una relación binaria < en T (llamada "precedencia") se llama marco . Un modelo está dado por el triple ( T , <, V ) de un marco y una función V llamada valoración que asigna a cada par ( a , u ) de una fórmula atómica y un valor temporal algún valor de verdad. La noción " ϕ es verdadero en un modelo U = ( T , <, V ) en el tiempo u " se abrevia U ϕ [ u ]. Con esta notación, [14]

Dada una clase F de marcos, una oración ϕ de TL es

Muchas oraciones son válidas únicamente para una clase limitada de marcos. Es común restringir la clase de marcos a aquellos con una relación < que sea transitiva , antisimétrica , reflexiva , tricotómica , irreflexiva , total , densa o alguna combinación de estas.

Una lógica axiomática mínima

Burgess describe una lógica que no hace suposiciones sobre la relación <, pero permite deducciones significativas, basadas en el siguiente esquema axiomático: [15]

  1. A donde A es una tautología de lógica de primer orden
  2. G( AB )→( GAGB )
  3. H( AB )→( HAHB )
  4. A →GP A
  5. AHFA

con las siguientes reglas de deducción:

  1. dado AB y A , deducir B ( modus ponens )
  2. Dada una tautología A , inferir G A
  3. Dada una tautología A , inferir H A

Se pueden derivar las siguientes reglas:

  1. Regla de Becker : dado AB , deducir T A →T B donde T es un tiempo , cualquier secuencia formada por G, H, F y P.
  2. Reflejo : dado un teorema A , deducir su enunciado reflejado A § , que se obtiene reemplazando G por H (y por tanto F por P) y viceversa.
  3. Dualidad : dado un teorema A , deducir su enunciado dual A *, que se obtiene intercambiando ∧ con ∨, G con F y H con P.

Traducción a la lógica de predicados

Burgess ofrece una traducción Meredith de enunciados en lógica de primer orden a enunciados en lógica de primer orden con una variable libre x 0 (que representa el momento presente). Esta traducción M se define recursivamente de la siguiente manera: [16]

donde es la oración A con todos los índices variables incrementados en 1 y es un predicado de un lugar definido por .

Operadores temporales

La lógica temporal tiene dos tipos de operadores: operadores lógicos y operadores modales. [17] Los operadores lógicos son operadores veritativo-funcionales habituales ( ). Los operadores modales utilizados en la lógica temporal lineal y la lógica de árboles computacionales se definen de la siguiente manera.

Símbolos alternativos:

Los operadores unarios son fórmulas bien formadas siempre que B( φ ) esté bien formada. Los operadores binarios son fórmulas bien formadas siempre que B( φ ) y C( φ ) estén bien formadas.

En algunas lógicas, algunos operadores no se pueden expresar. Por ejemplo, el operador N no se puede expresar en la lógica temporal de acciones .

Lógica temporal

Las lógicas temporales incluyen:

Una variación, estrechamente relacionada con las lógicas temporales, cronológicas o de tiempo, son las lógicas modales basadas en la “topología”, el “lugar” o la “posición espacial”. [23] [24]

Véase también

Notas

  1. ^ Vardi 2008, pág. 153
  2. ^ abc Vardi 2008, pág. 154
  3. ^ ab Łoś, Jerzy (1947). "Podstawy análisis metodológicoznej kanonów Milla". Zasoby Biblioteki Głównej Umcs (en polaco). nakł. Uniwersytetu Marii Curie-Skłodowskiej.
  4. ^ abcd Øhrstrøm, Peter (2019). "La importancia de las contribuciones de ANPrior y Jerzy Łoś en la historia temprana de la lógica temporal moderna". Lógica y filosofía del tiempo: más temas de Prior, volumen 2. Lógica y filosofía del tiempo. ISBN 9788772102658.
  5. ^ Peter Øhrstrøm; Per FV Hasle (1995). Lógica temporal: de las ideas antiguas a la inteligencia artificial . Springer. ISBN 978-0-7923-3586-3.págs. 176–178, 210
  6. ^ ab Rescher, Nicholas; Garson, James (enero de 1969). "Lógica topológica". Revista de lógica simbólica . 33 (4): 537–548. doi :10.2307/2271360. ISSN  0022-4812. JSTOR  2271360. S2CID  2110963.
  7. ^ "Lógica temporal (Enciclopedia de filosofía de Stanford)". Plato.stanford.edu . Consultado el 30 de julio de 2014 .
  8. ^ Walter Carnielli; Claudio Pizzi (2008). Modalidades y multimodalidades. Springer. pág. 181. ISBN 978-1-4020-8589-5.
  9. ^ Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italia, 30 de agosto – 4 de septiembre de 2009, Tutorial Lectures. Springer. pág. 112. ISBN 978-3-642-03753-5.
  10. ^ ab Tkaczyk, Marcin; Jarmużek, Tomasz (2019). "Cálculo posicional de Jerzy Łoś y el origen de la lógica temporal". Lógica y Filosofía Lógica . 28 (2): 259–276. doi : 10.12775/LLP.2018.013 . ISSN  2300-9802.
  11. ^ Prior, Arthur Norman (2003). Tiempo y modalidad: las conferencias John Locke de 1955-1956, dictadas en la Universidad de Oxford . Oxford: The Clarendon Press. ISBN 9780198241584.OCLC 905630146  .
  12. ^ Lawford, M. (2004). "Introducción a la lógica temporal" (PDF) . Departamento de Ciencias de la Computación, Universidad McMaster .
  13. ^ Goranko, Valentin; Galton, Antony (2015). Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy (edición de invierno de 2015). Metaphysics Research Lab, Universidad de Stanford.
  14. ^ Müller, Thomas (2011). "Lógica temporal o temporal" (PDF) . En Horsten, Leon (ed.). El compañero continuo de la lógica filosófica . A&C Black. pág. 329.
  15. ^ Burgess, John P. (2009). Lógica filosófica . Princeton, Nueva Jersey: Princeton University Press. p. 21. ISBN 9781400830497.OCLC 777375659  .
  16. ^ Burgess, John P. (2009). Lógica filosófica . Princeton, Nueva Jersey: Princeton University Press. p. 17. ISBN 9781400830497.OCLC 777375659  .
  17. ^ "Lógica temporal". Stanford Encyclopedia of Philosophy . 7 de febrero de 2020 . Consultado el 19 de abril de 2022 .
  18. ^ ab Maler, O.; Nickovic, D. (2004). "Monitoreo de propiedades temporales de señales continuas". doi :10.1007/978-3-540-30206-3_12.
  19. ^ Mehrabian, Mohammadreza; Khayatian, Mohammad; Shrivastava, Aviral; Eidson, John C.; Derler, Patricia; Andrade, Hugo A.; Li-Baboud, Ya-Shian; Griffor, Edward; Weiss, Marc; Stanton, Kevin (2017). "Lógica temporal de marca de tiempo (TTL) para probar la sincronización de sistemas ciberfísicos". Transacciones ACM sobre sistemas informáticos integrados . 16 (5s): 1–20. doi : 10.1145/3126510 . S2CID  3570088.
  20. ^ Koymans, R. (1990). "Especificación de propiedades en tiempo real con lógica temporal métrica", Real-Time Systems 2 (4): 255–299. doi :10.1007/BF01995674.
  21. ^ Li, Xiao, Cristian-Ioan Vasile y Calin Belta. "Aprendizaje por refuerzo con recompensas de lógica temporal". doi :10.1109/IROS.2017.8206234
  22. ^ Clarkson, Michael R.; Finkbeiner, Bernd; Koleini, Masoud; Micinski, Kristopher K.; Rabe, Markus N.; Sánchez, César (2014). "Lógicas temporales para hiperpropiedades". Principios de Seguridad y Confianza . Apuntes de conferencias sobre informática. vol. 8414, págs. 265–284. doi :10.1007/978-3-642-54792-8_15. ISBN 978-3-642-54791-1.S2CID8938993  .​
  23. ^ Rescher, Nicholas (1968). "Lógica topológica". Temas de lógica filosófica . págs. 229-249. doi :10.1007/978-94-017-3546-9_13. ISBN 978-90-481-8331-9.
  24. ^ von Wright, Georg Henrik (1979). "Una lógica modal del lugar". La filosofía de Nicholas Rescher . págs. 65–73. doi :10.1007/978-94-009-9407-2_9. ISBN 978-94-009-9409-6.

Referencias

Lectura adicional

Enlaces externos