Comunicaciones

Resumen

Sesión Lógica y Computabilidad

Semántica algebraica para un fragmento de la lógica intuicionista dinámica concurrente

Rocío Elizabeth Wagner

Universidad Nacional de La Pampa, Argentina   -   Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.

La lógica Proposicional dinámica (PDL) [1] es un sistema lógico basado en la lógica clásica definido sobre un lenguaje de programas. A cada programa $\alpha$ se le asocia un conector modal $[\alpha]$ donde la fórmula $[\alpha]\varphi$ significa: después de cada ejecución de $\alpha$, $\varphi$ es verdad. Se parte de programas atómicos y se forman nuevos programas a través de ciertas operaciones entre programas. Una extensión de la PDL, llamada lógica concurrente proposicional dinámica (CDPL), fue considerada por Pelag [2], agregando una operación entre programas, la cual fue estudiada principalmente por R.Goldblatt en [3],[4]. La CPDL está basada en la lógica clásica, aquí consideraremos una versión de las lógicas proposicionales dinámicas concurrentes basadas en la lógica intuicionista (ICPDL) con un solo programa ([5],[6]). En esta comunicación presentaremos semánticamente un nuevo fragmento de las ICPDL con un solo programa. Daremos una axiomatización a través de un sistema al estilo Hilbert y extendiendo las nociones estudiadas por Sergio Celani en [7] para álgebras de Boole concurrentes, presentaremos a las Álgebras de Heyting concurrentes o CH-álgebras, las cuales forman una semántica algebraica para dicho fragmento de ICPDL. Hemos desarrollado dos semánticas relacionales, los ic-marcos y los IKN-marcos. Aquí, nos centraremos en los ic-marcos. Presentaremos un tipo de espacio topológico (Espacios de Esakia concurrentes) basados en los ic-marcos, los cuales son una representación topológica de las CH-álgebras. Definiremos la categoría de las CH-álgebras y la categoría de los Espacios de Esakia concurrentes, y veremos que estas categorías son dualmente equivalentes.

Trabajo en conjunto con: Luciano González (Universidad Nacional de La Pampa, Argentina) y Sergio Celani (Universidad Nacional del Centro de la provincia de Buenos Aires, Argentina).

Referencias

[1] V. R. Pratt. Semantical considerations on Floyd-Hoare logic. In 17th Annual Symposium on Foundations of Computer Science, pages 109-121. IEEE, 1976.

[2] D. Peleg. Concurrent dynamic logic. Journal of the Association for Computing Machin ery, 34(2):450-479, 1987.

[3] R. Goldblatt. Logics of time and computation, volume 7 of Lecture Notes. CSLI, second edition edition, 1992.

[4] R. Goldblatt. Parallel action: Concurrent dynamic logic with independent modalities. Studia Logica, 51:551-578, 1992.

[5] D. Wijesekera. Constructive modal logics I. Ann. of Pure Appl. Logic, 50(3):271-301, 1990.

[6] D. Wijesekera and A. Nerode. Tableaux for constructive concurrent dynamic logic. Ann. Pure Appl. Logic, 135(1-3):172, 2005.

[7] S. Celani. Concurrent algebras: an algebraic study of a fragment of concurrent propo sitional dynamic logic. Algebra Universalis, 66:183-204, 2011.

Ver resumen en PDF