UMA 2022
Una lógica temporal es cualquier sistema formal (de axiomas y/o reglas) que permite representar y razonar acerca de proposiciones cualificadas en términos del tiempo. La lógica temporal tiene importantes aplicaciones en el campo de la verificación formal donde es utilizada para establecer requerimientos de sistemas de hardware o software. La lógica minimal temporal ( minimal tense logic) a la que da lugar el sistema $K_t$ de E. J. Lemmon, establece un conjunto de relaciones mínimas entre los operadores $G$ (``siempre será el caso que'') y $H$ (``siempre ha sido el caso que''). Por lo que, toda lógica temporal resulta ser una extensión de $K_t$.
Por otra parte, un álgebra temporal es una estructura (1) $\langle A, H, G\rangle$ donde $A$ es un álgebra de Boole; y $H$ y $G$ son operadores unarios definidos sobre $A$ que verifican las identidades: $$G1\approx 1 \hspace{1cm} H1\approx 1 $$ $$G(x\wedge y)\approx Gx \wedge Gy \hspace{1cm} H(x\wedge y)\approx Hx \wedge Hy $$ $$\neg x \vee G\neg H\neg x\approx 1 \hspace{1cm} \neg x \vee H\neg G\neg x\approx 1$$
Si en lugar de tomar un álgebra de Boole en (1), tomamos un álgebra de De Morgan (Heyting, Nelson etc.) obtenemos una nueva clase de estructura (algebraica) temporal.
En este trabajo nos interesamos en la lógica que preserva grados de verdad con respecto a diferentes estructuras temporales. En primer lugar, probamos que la lógica que preserva grados de verdad con respecto a las álgebras temporales es precisamente $K_t$. Además, presentamos un cálculo de secuentes correcto y completo con respecto a este sistema y hacemos lo propio para otras clases de estructuras temporales. Finalmente presentamos algunos cálculos de secuentes libres de corte para fragmentos de dichos sistemas.
Trabajo en conjunto con: Aldo V. Figallo (Universidad Nacional del Sur, Argentina) y Martín Figallo (Universidad Nacional de San Juan, Argentina).
Referencias
[1] Figallo, A. V., & Pelaitay, G. (2013). Tense operators on De Morgan algebras. Logic Journal of IGPL 22(2):255--267.
[2] Jarvinen, J., Kondo, M. & Kortelainen, J. (2008). Logics from Galois connections. International Journal of Approximate Reasoning 49:595--606
[3] Kowalski T. (1998). Varieties of tense algebras, Reports on Mathematical Logic 32:53--95.
[4] Sadrzadeh, M., & Dyckhoff, R. (2009). Positive logic with adjoint modalities: proof theory, semantics and reasoning about information. Electronic Notes of Theoretical Computer Science, 249: 451--470.