Lógica tensa
La lógica temporal es una extensión de la lógica modal, la cual es prácticamente usada en sistemas de reglas, donde está presente el tiempo. Existe una cierta relación con otras variedades de lógica, por ejemplo, la lógica modal. Su estudio tiene importancia en la informática hasta nuestros días.
Por ejemplo, tomemos la sentencia: "Tengo hambre"; aunque su significado es independiente del tiempo, el valor de verdad o falsedad de la misma puede variar con el tiempo en un determinado sistema que incluya acciones de comer; así, en función del sistema, algunas veces será cierta y otras falsa, aunque nunca será cierta y falsa simultáneamente.
La lógica temporal fue estudiada por Aristóteles, en algunos de sus escritos hay expresiones que guardan una cierta analogía con la lógica temporal de primer orden; es de esta manera como aparecen expresiones con cuantificadores existenciales y cuantificadores universales
En lógica temporal aparecen los mismos operadores que en una lógica de primer orden, junto con otros nuevos, entre los que se pueden encontrar: Siempre, algunas veces y nunca.
Algunos sistemas lógicos basados en lógica temporal son: Lógica computacional en árbol (Computational tree logic, CTL), lógica lineal temporal (Linear temporal logic, LTL) y Lógica temporal de intervalos (Interval temporal logic, ITL). Lógica de acciones temporal (Temporal Logic of Actions, TLA).
La lógica temporal tiene dos clases de operadores: operadores lógicos y operadores modales [1]. Los operadores lógicos son usualmente operadores truth-functional (). Los operadores modales usan el Linear Temporal Logic y Computation Tree Logic son definidos como sigue.
Símbolos alternativos:
Operadores unarios son well-formed formulas cuandoquiera que B() es bien formado. Los operadores binarios son fórmulas bien formadas cuandoquiera que B() y C() son bien formadas.
En algunas lógicas, algunos operadores no pueden se expresados. Por ejemplo, el operador N no puede ser expresado en la Temporal Logic of Actions.
En la figura se muestra una estructura de Kripke de tres estados. Se puede describir de la siguiente manera:
Si se considera arbitrariamente al estado rojo como estado inicial, se cumple lo siguiente: