Sesión Lógica y Computabilidad
Miércoles 20 de septiembre
Mañana - Lugar: Anfiteatro I
| Horario | Título | Expositor/a |
|---|---|---|
| 8:40 ~ 9:20 | La bisimilitud entre árboles de rango $\omega+2$ no es suave | Pedro Sánchez Terraf |
| 9:20 ~ 9:40 | Extensiones expresivas de Propositional Dynamic Logic a través de propiedades topológicas de grafos | Edwin Pin |
| 9:40 ~ 10:00 | On the construction of $3\times 3$--valued Łukasiewicz-Moisil algebras | Carlos Gallardo |
| 10:30 ~ 11:10 | Local quantum field logic | Hector Freytes |
| 11:10 ~ 11:30 | Lógicas de Descripción sobre Grafos de Datos | Juliana Putero |
| 11:30 ~ 11:50 | A categorical equivalence for tense pseudocomplemented distributive lattices | Maia Starobinsky |
Tarde - Lugar: Aula 55
| Horario | Título | Expositor/a |
|---|---|---|
| 15:00 ~ 15:40 | Teoría de prueba en el contexto de paraconsistencia con operador de consistencia fuerte | Martín Figallo |
| 15:40 ~ 16:00 | Una lógica modal explícita de preferencias y razones | Sebastian Ferrando |
| 16:00 ~ 16:20 | Semántica de las $F_{1}$-estructuras para los cálculos paraconsistentes $C_{n}$, $n\ge 2$ | Andrea Carina Murciano |
| 16:20 ~ 16:40 | Productos twist y rotaciones | Miguel Andrés Marcos |
Jueves 21 de septiembre
Mañana -
| Horario | Título | Expositor/a |
|---|---|---|
| 9:00 ~ 9:40 | Introducción a los asistentes de pruebas basados en teoría de tipos dependientes, en específico "Coq'' (y resultados parciales sobre Redex $\rightarrow$ Coq) | Mallku Soldevila |
| 9:40 ~ 10:00 | Generalizando el Framework de Katzuno y Mendelzon para AGM con un enfoque semántico | Daniel Grimaldi |
| 10:30 ~ 10:50 | A Topological Study of $k$-rough Heyting Algebras | Florencia Valverde |
| 10:50 ~ 11:10 | Characterization of Subdirectly Irreducible Heyting Algebras with Negative Tense Operators | Gustavo Pelaitay |
| 11:10 ~ 11:30 | Ordenes subyacentes a bandas regulares a derecha | Joel Kuperman |
Charlas invitadas
Miércoles 20 de septiembre, 8:40 ~ 9:20
La bisimilitud entre árboles de rango $\omega+2$ no es suave
Pedro Sánchez Terraf
Universidad Nacional de Córdoba -- CIEM-FAMAF, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
Es bien sabido que la lógica modal básica ($\mathsf{BML}$) caracteriza la relación de bisimilitud entre marcos de Kripke punteados tales que cada punto tiene finitos sucesores por cada relación de accesibilidad. Es decir, si los “puntos'' de sendos marcos satisfacen las mismas fórmulas de $\mathsf{BML},$ entonces existe una bisimulación entre estos últimos que contiene el par de aquellos. También existen contraejemplos estándares a esta caracterización lógica cuando alguna relación de accesibilidad tiene infinitos sucesores. A su vez, esto se soluciona permitiendo conjunciones (y disyunciones) numerables, obteniendo la lógica infinitaria $\mathsf{BML}_\omega$. Esta lógica tiene una cantidad incontable de fórmulas, y es de interés saber si algún fragmento contable es suficiente para caracterizar la bisimilitud.
En esta comunicación veremos que aún restringiéndose a cierta familia de marcos bien fundados y de “profundidad'' acotada (como en el título), no existe un tal fragmento contable. La prueba utiliza conceptos básicos de Teoría de Conjuntos Descriptiva.
Trabajo en conjunto con: Martín Moroni (Universidad Nacional de Córdoba).
Miércoles 20 de septiembre, 10:30 ~ 11:10
Local quantum field logic
Hector Freytes
Università degli Studi di Cagliari, Italia - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
Algebraic quantum field theory, or AQFT for short, is a rigorous analysis of the structure of relativistic quantum mechanics [4]. It is formulated in terms of a net of operator algebras indexed by regions of a Lorentzian manifold. In several cases the mentioned net is represented by a family of von Neumann algebras, concretely, type III factors. In this perspective, a logical system can be established capturing the propositional structure encoded in the algebras of the mentioned net. In this framework, this work contributes to the solution of a family of open problems, emerged since the 30s, about the characterization of those logical systems which can be identified with the lattice of projectors arising from the Murray-von Neumann classification of factors [1,2,3]. More precisely, based on physical requirements formally described in AQFT, an equational theory able to characterize the type III condition in a factor is provided. This equational system motivates the study of a variety of algebras, concretely a discriminator variety, having an underlying orthomodular lattice structure. A Hilbert style calculus, algebraizable in the mentioned variety, is also introduced and a corresponding completeness theorem is established.
Referencias
[1] L. J. Bunce, J. D. Maitland Wright, Quantum Logic, State Space Geometry and Operator Algebras, Comm. Math. Phys. 96 (1984) 345-348.
[2] H. Gross, Hilbert lattices: New results and unsolved problems, Found. Phys. 20 (1990), 529-559.
[3] S. Holland, The Current Interest in Orthomodular Lattices, in: J. C. Abbott, (ed), Trends in Lattice Theory, Van Nostrand-Reinhold, New York (1970) pp. 41-26.
[4] J. Yngvason, The role of type III factors in quantum field theory, Rep. Math. Phys. 55 (2005), 135-147.
Miércoles 20 de septiembre, 15:00 ~ 15:40
Teoría de prueba en el contexto de paraconsistencia con operador de consistencia fuerte
Martín Figallo
Universidad Nacional del Sur, Departamento de Matemática, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
El enfoque de Newton da Costa a la paraconsistencia, hoy globalmente conocida como ''Escuela Brasileña de Paraconsistencia'', fue generalizado de modo natural por W. Carnielli y J. Marcos con la noción de Lógicas de la Inconsistencia Formal (LFI). Estas son lógicas paraconsistentes que internalizan las nociones de consistencia e inconsistencia a nivel del lenguaje objeto.
Por otro lado, A. Avron, B. Konikowska y A. Zamansky ([2]) estudiaron de forma sistemática y modular la teoría de prueba de una familia grande de LFIs. Más precisamente, presentaron cálculos de secuentes con la propiedad de eliminación de corte para las versiones proposicionales de estas lógicas. Sin embargo, como estos mismos autores observaron, para desarrollar herramientas eficientes que permitan el razonamiento automatizado bajo incertidumbre (theorem provers) es importante desarrollar la teoría de prueba de las versiones de primer orden de estas LFIs.
En esta comunicación, damos un primer paso en este sentido. Esto es, estudiamos la teoría de prueba de la versión de primer orden de una LFI 3-valorada con operador de consistencia fuerte, que fuera desarrollada en el contexto del estudio de bases de datos inconsistentes ([3]). Entre otras cosas, presentaremos un cálculo de secuentes correcto y completo con la propiedad de eliminación de corte; y mostraremos algunas aplicaciones.
Trabajo en conjunto con: Victoria Arce Pistone (Universidad Nacional del Sur, Bahía Blanca, Argentina).
Referencias
[1] Arce Pistone, V. and Figallo, M. (2023). Proof-theoretic aspects of paraconsistency with strong consistency operator. http://arxiv.org/abs/2304.11481
[2] Avron, A., Konikowska, B. and Zamansky, A. (2012). Modular Construction of Cut-Free Sequent Calculi for Paraconsistent Logics. Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, 85–94
[3] Carnielli, W. A., Marcos, J. and de Amo, S. (2000). Formal inconsistency and evolutionary databases. Logic and Logical Philosophy, 8, 115–152.
Jueves 21 de septiembre, 9:00 ~ 9:40
Introducción a los asistentes de pruebas basados en teoría de tipos dependientes, en específico "Coq'' (y resultados parciales sobre Redex $\rightarrow$ Coq)
Mallku Soldevila
FAMAF, Universidad Nacional de Córdoba, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
En esta comunicación comenzaremos recorriendo brevemente ideas que surgieron en la matemática durante la primera mitad del siglo pasado, y en términos de las cuales podemos justificar la implementación de un asistente de pruebas basado en teoría de tipos dependientes. Revisaremos conceptos de lógica intuicionista, lambda-cálculo y teoría de tipos, lo que nos permitirá entender las razones por las cuales podemos admitir (ciertos) programas en un lenguaje con tipos dependientes, como análogos computacionales de las pruebas que escribimos en papel.
A continuación introduciremos "Coq": un asistente de pruebas basado en teoría de tipos dependientes, ampliamente utilizado en esfuerzos de formalización de semántica de lenguajes de programación reales. Revisaremos construcciones fundamentales del "Cálculo de Construcciones Inductivas" (el lenguaje y semántica fundacional de Coq), mencionaremos sus propiedades teóricas principales, y estudiaremos ejemplos de definiciones de tipos inductivos, proposiciones y una demostración.
Finalmente comentaremos, de manera breve, sobre los primeros pasos dados en el desarrollo de una herramienta para automatizar la traducción de un modelo de semántica de reducciones en Redex, hacia un modelo (idealmente) semánticamente equivalente en Coq. La intención es proporcionar automatización a (algunas partes) de la certificación de propiedades fundamentales de tales modelos.
Trabajo en conjunto con: Dr. Beta Ziliani (FAMAF, UNC y Manas.Tech, Argentina).
Referencias
[1] Casey Klein, Jay McCarthy, Steven Jaconette, Robert Bruce Findler (2011) A semantics for context- sensitive reduction semantics. En: APLAS’11.
Resúmenes
Miércoles 20 de septiembre, 8:40 ~ 9:20
La bisimilitud entre árboles de rango $\omega+2$ no es suave
Pedro Sánchez Terraf
Universidad Nacional de Córdoba -- CIEM-FAMAF, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
Es bien sabido que la lógica modal básica ($\mathsf{BML}$) caracteriza la relación de bisimilitud entre marcos de Kripke punteados tales que cada punto tiene finitos sucesores por cada relación de accesibilidad. Es decir, si los “puntos'' de sendos marcos satisfacen las mismas fórmulas de $\mathsf{BML},$ entonces existe una bisimulación entre estos últimos que contiene el par de aquellos. También existen contraejemplos estándares a esta caracterización lógica cuando alguna relación de accesibilidad tiene infinitos sucesores. A su vez, esto se soluciona permitiendo conjunciones (y disyunciones) numerables, obteniendo la lógica infinitaria $\mathsf{BML}_\omega$. Esta lógica tiene una cantidad incontable de fórmulas, y es de interés saber si algún fragmento contable es suficiente para caracterizar la bisimilitud.
En esta comunicación veremos que aún restringiéndose a cierta familia de marcos bien fundados y de “profundidad'' acotada (como en el título), no existe un tal fragmento contable. La prueba utiliza conceptos básicos de Teoría de Conjuntos Descriptiva.
Trabajo en conjunto con: Martín Moroni (Universidad Nacional de Córdoba).
Miércoles 20 de septiembre, 9:20 ~ 9:40
Extensiones expresivas de Propositional Dynamic Logic a través de propiedades topológicas de grafos
Edwin Pin
Universidad de Buenos Aires, Instituto de Ciencias de la Computación, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
El sistema formal $\textit{Propositional Dynamic Logic}$ [2], $\text{PDL}$ en adelante, surgió como un lenguaje basado en lógica modal para describir correctitud, terminación y equivalencia de programas. Desde su origen se ha aplicado también con otros propósitos, por ejemplo, como lenguaje de consulta sobre estructuras con forma de grafos [3]. Otro punto importante en el estudio de este lenguaje es lo fácil que se puede adaptar sintácticamente según determinadas necesidades ontológicas a estudiar, como es el caso de [4] donde analizan $\text{ICPDL}$: $\text{PDL}$ + Intersection + Converse. La adhesión de estos nuevos operadores no solo incrementa el poder expresivo de $\text{PDL}$ sino que preservan varias de las propiedades computacionales que $\text{PDL}$ posee.
Más recientemente, en [1] se introdujo el lenguaje $\text{CPDL}^+$ como una extensión de $\text{PDL}$ dotado con un operador nuevo denominado $\textit{programa conjuntivo}$, que es compatible con los demás operadores de $\text{PDL}$ y cuyo propósito es consultar sobre cualquier estructura de Kripke si determinados patrones relativos a grafos con datos surgen en el modelo. Para ello el operador de programa conjuntivo se define junto a la noción de $\textit{grafo subyacente}$ de un programa y bajo este esquema se estudiaron distintos problemas: (1) definición de fragmentos de $\text{CPDL}^+$ mediante propiedades topológicas de grafos, (2) indistinguibilidad de modelos con respecto a fragmentos de $\text{CPDL}^+$ mediante criterios de bisimulación, (3) satisfacibilidad de $\text{CPDL}^+$ y de sus fragmentos, (4) model checking. Los problemas computacionales relacionados a (3) y (4) se demostraron decidibles según el fragmento escogido. Más aún, $\text{CPDL}^+$ es un lenguaje altamente abarcativo, pues contiene a $\text{ICPDL}$, a varias otras extensiones de $\text{PDL}$, y además a algunos lenguajes de interés en el área de bases de datos con forma de grafos, como $\text{C2RPQ}$ [6].
Por lo general, un fragmento de una lógica se obtiene por medio de restricciones sintácticas, pero en el caso de $\text{CPDL}^+$ se pueden definir fragmentos que dependen de características topólogicas impuestas sobre los grafos subyacentes de los programas conjuntivos. En este sentido definimos $\text{CPDL}^+(\mathcal{G})$ como el fragmento de $\text{CPDL}^+$ cuyos programas conjuntivos tienen grafos subyacentes pertenecientes a una clase de grafos $\mathcal{G}$. Una propiedad importante de grafos usada ampliamente en [1] es ``bounded treewidth'', siendo el treewidth de un grafo un parámetro entero que indica qué tan similar es dicho grafo a un árbol [5]. De esta manera, podemos ver a $\text{CPDL}^+$ como la unión de una jerarquía de fragmentos que denotamos $\text{CPDL}^+(\text{TW}_k)$, donde $\text{TW}_k$ es la clase de todos los grafos de treewidth a lo sumo $k$. Bajo esta noción y considerando grafos subyacentes conexos, se demostró que $\text{ICPDL}$ es equiexpresivo a $\text{CPDL}^+(\text{TW}_k)$ para $k = 1, 2$ (i.e. toda fórmula de $\text{ICPDL}$ es equivalente a otra en $\text{CPDL}^+(\text{TW}_k)$ y viceversa). Por otra parte, también se demostró que para todo $k \geq 2$, $\text{CPDL}^+(\text{TW}_k)$ es menos expresivo que $\text{CPDL}^+(\text{TW}_{k+1})$. Para estos fragmentos se estudiaron los problemas especificados en los ítems (2-4). En particular se tienen los siguientes resultados: (2) Para cada $k$, se obtuvo un criterio de indistinguibilidad de modelos para $\text{CPDL}^+(\text{TW}_k)$ en términos de un juego de $k$-piedras, también denominado $k$-$\textit{bisimulación}$. (3) Se demostró que para todo $k$, el problema de satisfacibilidad de $\text{CPDL}^+(\text{TW}_k)$ es decidible en complejidad $\text{2ExpTime}$ , que es igual a la de $\text{ICPDL}$ [4]. (4) El problema de model checking sobre estructuras finitas es polinomial para cualquier $\text{CPDL}^+(\text{TW}_k)$, pero es $\text{NP-hard}$ para $\text{CPDL}^+$.
Trabajo en conjunto con: Diego Figueira (University of Bordeaux, CNRS-LaBRI, France) y Santiago Figueira (Universidad de Buenos Aires, DC, CONICET, ICC).
Referencias
[1] Diego Figueira, Santiago Figueira, and Edwin Pin. PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse. In Annual Symposium on Logic in Computer Science (LICS), Proceedings of Annual Symposium on Logic in Computer Science (LICS), Boston, United States, June 2023.
[2] Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194–211, 1979.
[3] Martin Lange. Model checking propositional dynamic logic with all extras. J. Appl. Log., 4(1):39– 49, 2006.
[4] Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with intersection and converse: satisfiability and infinite-state model checking. 74(1):279–314, 2009.
[5] Umberto Bertele and Francesco Brioschi. On non-serial dynamic programming. Journal of Combinatorial Theory, Series A, 14(2):137–148, 1973.
[6] Meghyn Bienvenu, Magdalena Ortiz and Mantas Simkus. Conjunctive Regular Path Queries in Lightweight Description Logics. IJCAI '13: Proceedings of the Twenty-Third international joint conference on Artificial Intelligence Pages 761–767, August 2013.
Miércoles 20 de septiembre, 9:40 ~ 10:00
On the construction of $3\times 3$--valued Łukasiewicz-Moisil algebras
Carlos Gallardo
Universidad Nacional del Sur, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
In 1971, Georgescu and Vraciu [1] introduced a new class of algebras which they called monadic n-valued Łukasiewicz–Moisil algebras. This subject caused great interest and Figallo and Sanza [2] introduced and investigated monadic $n\times m$-valued Łukasiewicz–Moisil algebras which constitute a generalization of them. In this note, we construct a $3\times 3$--valued Łukasiewicz-Moisil algebras from a monadic $3\times 3$--valued Łukasiewicz-Moisil algebras, generalizing A. Monteiro's construction. Besides, we construct a monadic $3\times 3$--valued Łukasiewicz-Moisil algebras from a monadic $n\times m$--valued Łukasiewicz-Moisil algebras, generalizing V. Boicescu's construction.
Referencias
[1] G. Georgescu, C. Vraciu, Algebre Boole monadice si algebre Łukasiewicz monadice, Studii Cerc. Mat., 23, 1025-1048 (1971)
[2] A.V. Figallo, C. Sanza, Monadic nxm-valued Łukasiewicz-Moisil algebras, Mathematica Bohemica, 4, 425-447 (2012)
Miércoles 20 de septiembre, 10:30 ~ 11:10
Local quantum field logic
Hector Freytes
Università degli Studi di Cagliari, Italia - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
Algebraic quantum field theory, or AQFT for short, is a rigorous analysis of the structure of relativistic quantum mechanics [4]. It is formulated in terms of a net of operator algebras indexed by regions of a Lorentzian manifold. In several cases the mentioned net is represented by a family of von Neumann algebras, concretely, type III factors. In this perspective, a logical system can be established capturing the propositional structure encoded in the algebras of the mentioned net. In this framework, this work contributes to the solution of a family of open problems, emerged since the 30s, about the characterization of those logical systems which can be identified with the lattice of projectors arising from the Murray-von Neumann classification of factors [1,2,3]. More precisely, based on physical requirements formally described in AQFT, an equational theory able to characterize the type III condition in a factor is provided. This equational system motivates the study of a variety of algebras, concretely a discriminator variety, having an underlying orthomodular lattice structure. A Hilbert style calculus, algebraizable in the mentioned variety, is also introduced and a corresponding completeness theorem is established.
Referencias
[1] L. J. Bunce, J. D. Maitland Wright, Quantum Logic, State Space Geometry and Operator Algebras, Comm. Math. Phys. 96 (1984) 345-348.
[2] H. Gross, Hilbert lattices: New results and unsolved problems, Found. Phys. 20 (1990), 529-559.
[3] S. Holland, The Current Interest in Orthomodular Lattices, in: J. C. Abbott, (ed), Trends in Lattice Theory, Van Nostrand-Reinhold, New York (1970) pp. 41-26.
[4] J. Yngvason, The role of type III factors in quantum field theory, Rep. Math. Phys. 55 (2005), 135-147.
Miércoles 20 de septiembre, 11:10 ~ 11:30
Lógicas de Descripción sobre Grafos de Datos
Juliana Putero
FAMAF - Universidad Nacional de Córdoba, y CONICET, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
La tarea de representar y manipular información de manera compacta y eficiente resulta, en general, compleja desde un punto de vista computacional. En este sentido, es de gran interés y utilidad contar con modos eficientes de almacenamiento y con mecanismos que permitan inferir propiedades acerca de dicha información. El desarrollo y estudio de representaciones compactas de datos, como así también de procedimientos eficientes para su manipulación, pueden ser abordados desde un punto de vista formal utilizando herramientas de la lógica. En particular, uno de los enfoques más utilizados en la práctica, es el basado en las llamadas Lógicas de Descripción [1] .
Las Lógicas de Descripción fueron diseñadas con el propósito de describir abstracciones de algún dominio de interés. En general, dichas abstracciones están constituidas por tres componentes principales: Conceptos, que representan conjuntos de elementos; Nombres de Roles, que representan relaciones binarias entre elementos; e Individuos, que representan elementos específicos del dominio.
Por ejemplo, consideremos un dominio de datos sobre la estructura de la currícula de una carrera universitaria. La Lógica de Descripción nos permite construir expresiones de la forma $\exists \mathsf{teaches.Course}$, donde Course es un concepto y teaches es un rol. De esta manera, la expresión caracteriza a “los elementos del dominio que corresponden con individuos que enseñan algún curso”. Este tipo de expresiones de la Lógica de Descripción se combinan luego para definir las bases de conocimiento que proveen descripciones abstractas de la información concreta contenida, por ejemplo, en una base de datos. Una base de conocimiento es un par $K= (T, A)$ denominados TBox y ABox, respectivamente. La TBox contiene las condiciones generales sobre el dominio de datos, mientras que la ABox puede entenderse como una descripción de elementos concretos de dicho dominio. Por ejemplo, expresiones del tipo $\forall \mathsf{teaches.Course} \sqsubseteq \mathsf{Teacher}$ pertenecen a la TBox, ya que denota la propiedad “quienes enseñan cursos son docentes”. Por su parte, una expresión $\mathsf{Mary:Teacher}$ pertenece a la ABox, ya que denota el hecho de que “Mary es docente”. Una vez definida una base de conocimiento sobre alguna Lógica de Descripción en particular, es interesante contar con mecanismos de inferencia eficientes para extraer información a partir de la misma. Por ejemplo, para verificar si un concepto está incluido en otro (tarea conocida como subsunción), o verificar si una base de conocimientos se encuentra libre de contradicciones (conocido como chequeo de consistencia). Para ello, se utilizan métodos lógicos, como pueden ser procedimientos basados en tableaux.
Sin embargo, tal como suele ocurrir a la hora de utilizar cualquier lenguaje lógico, la expresividad del mismo puede resultar insuficiente para el problema que se busca abordar. Por ejemplo, cuando se manipulan grandes cantidades de datos, es interesante comparar ciertos atributos que aparecen en los mismos, como pueden ser la cantidad de horas asignadas a cada estudiante o cada docente en el ejemplo mencionado anteriormente. En los enfoques tradicionales, la capacidad de comparar los valores de cada atributo se encuentra ausente. Es por ello que en este trabajo, y siguiendo las ideas propuestas en [2,3], extendemos lenguajes de descripción tradicionales con operadores que nos permiten comparar atributos de datos entre los elementos del dominio. De esta manera podemos contar con tal información en nuestras bases de conocimiento, interpretadas sobre los llamados Grafos de Datos. A su vez avanzamos con el estudio de mecanismos de inferencia basados en tableaux sobre este nuevo tipo de bases de conocimiento. Este enfoque nos permite además, estudiar la complejidad computacional de realizar inferencia con estas lógicas, como así también buscar fragmentos que admiten algoritmos eficientes de razonamiento.
Trabajo en conjunto con: Valentin Cassano (Universidad Nacional de Río Cuarto y CONICET, Argentina) y Raul Fervari (Universidad Nacional de Córdoba y CONICET, Argentina).
Referencias
[1] Baader, F., Horrocks, I., Lutz, C., & Sattler, U. An Introduction to Description Logic. Cambridge: Cambridge University Press (2017).
[2] Kostylev, E., Reutter, J., & Vrgoc, D. XPath for DL Ontologies. Proceedings of the AAAI Conference on Artificial Intelligence, 29 (2015).
[3] Areces, C., & Fervari, R. Axiomatizing Hybrid XPath with Data. Logical Methods in Computer Science (LMCS), volume 17, issue 3, 2021.
Miércoles 20 de septiembre, 11:30 ~ 11:50
A categorical equivalence for tense pseudocomplemented distributive lattices
Maia Starobinsky
Instituto de Ciencias Básicas, Universidad Nacional de San Juan y Facultad de Ciencias Económicas, Universidad de Buenos Aires, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
A pseudocomplemented distributive lattice (also known as a distributive $p$-algebra) is an algebraic structure denoted as $\langle A, \wedge, \vee, \ast, 0, 1 \rangle$, where the underlying structure $\langle A, \wedge, \vee, 0, 1 \rangle$ is a bounded distributive lattice, and the unary operation $\ast$ represents a pseudocomplement operation [1]. This operation satisfies the property that $x \wedge y = 0$ if and only if $x \leq y^\ast$.
In this paper, our motivation stems from the definition of tense operators on distributive lattices proposed by Chajda and Paseka in [2]. We introduce and explore the variety of tense pseudocomplemented distributive lattices. Specifically, we establish a categorical equivalence of these structures with a full subcategory of tense KAN-algebras.
Trabajo en conjunto con: Gustavo Pelaitay (Instituto de Ciencias Básicas, Universidad Nacional de San Juan y CONICET).
Referencias
[1] Balbes, R., Dwinger P., Distributive Lattices. University of Missouri Press (1974)
[2] I.Chajda, J.Paseka: Algebraic Appropach to Tense Operators, Research and Exposition in Mathematics Vol. 35, Heldermann Verlag (Germany), 2015, ISBN 978-3-88538-235-5.
Miércoles 20 de septiembre, 15:00 ~ 15:40
Teoría de prueba en el contexto de paraconsistencia con operador de consistencia fuerte
Martín Figallo
Universidad Nacional del Sur, Departamento de Matemática, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
El enfoque de Newton da Costa a la paraconsistencia, hoy globalmente conocida como ''Escuela Brasileña de Paraconsistencia'', fue generalizado de modo natural por W. Carnielli y J. Marcos con la noción de Lógicas de la Inconsistencia Formal (LFI). Estas son lógicas paraconsistentes que internalizan las nociones de consistencia e inconsistencia a nivel del lenguaje objeto.
Por otro lado, A. Avron, B. Konikowska y A. Zamansky ([2]) estudiaron de forma sistemática y modular la teoría de prueba de una familia grande de LFIs. Más precisamente, presentaron cálculos de secuentes con la propiedad de eliminación de corte para las versiones proposicionales de estas lógicas. Sin embargo, como estos mismos autores observaron, para desarrollar herramientas eficientes que permitan el razonamiento automatizado bajo incertidumbre (theorem provers) es importante desarrollar la teoría de prueba de las versiones de primer orden de estas LFIs.
En esta comunicación, damos un primer paso en este sentido. Esto es, estudiamos la teoría de prueba de la versión de primer orden de una LFI 3-valorada con operador de consistencia fuerte, que fuera desarrollada en el contexto del estudio de bases de datos inconsistentes ([3]). Entre otras cosas, presentaremos un cálculo de secuentes correcto y completo con la propiedad de eliminación de corte; y mostraremos algunas aplicaciones.
Trabajo en conjunto con: Victoria Arce Pistone (Universidad Nacional del Sur, Bahía Blanca, Argentina).
Referencias
[1] Arce Pistone, V. and Figallo, M. (2023). Proof-theoretic aspects of paraconsistency with strong consistency operator. http://arxiv.org/abs/2304.11481
[2] Avron, A., Konikowska, B. and Zamansky, A. (2012). Modular Construction of Cut-Free Sequent Calculi for Paraconsistent Logics. Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, 85–94
[3] Carnielli, W. A., Marcos, J. and de Amo, S. (2000). Formal inconsistency and evolutionary databases. Logic and Logical Philosophy, 8, 115–152.
Miércoles 20 de septiembre, 15:40 ~ 16:00
Una lógica modal explícita de preferencias y razones
Sebastian Ferrando
Universidad Nacional de Córdoba, CIFFyH., Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
En el lenguaje estándar de la lógica de la preferencia, se entiende que una fórmula como PA expresa simplemente una preferencia por la proposición A, o también puede decirse, por el estado de cosas o conjunto de mundos posibles asociado con esta proposición. Se puede admitir sin embargo, que en cada caso existe una razón para esta preferencia, que, no obstante, el lenguaje estándar de la lógica de la preferencia no puede denotar de forma explícita. En el lenguaje modal explícito de la Lógica de la Justificación, las modalidades del tipo de las representadas por el operador $\Box$ (box) se descomponen en términos, t, que denotan la razón específica por la que una proposición se estima que está justificada, demostrada, conocida, creída, etc. En el caso de las preferencias de un agente esto vendría a decir, que las fórmulas del tipo PA –esto es, que un agente manifiesta una preferencia por la proposición representada por A- se reemplazan por fórmulas del tipo t:A. Una lectura o interpretación informal de esto sería que t es una razón por la cual es preferida A, o que se prefiere A porque t. En este trabajo nos proponemos desarrollar una de estas lógicas de la preferencia, a saber, la lógica modal de preferencias ceteris paribus [2], como una lógica de preferencias con razones o justificaciones, en la forma de una lógica modal explícita. Recurrimos a tal fin a la lógica de preferencias [3] y a la realización de distintos sistemas modales dentro de esta última. Desde un costado filosófico, nuestro interés radica en abarcar formalmente un tipo de razonamiento en el que se consideren preferencias y razones o justificaciones para estas. Asimismo, buscamos incorporar en este marco formal-normativo la noción de `horizonte de preferencias', que von Wright esbozara en [1].
Referencias
[1] von Wright, G., “The logic of preference reconsidered”, Theory and Decision 3 (1972) 140-169.
[2] van Benthem, J., Girard, P., Roy, O., “Everything Else Being Equal: A Modal Logic for Ceteris Paribus Preferences”, J Philos Logic (2009) 38:83–125.
[3] Artemov, S, Fitting, M., Justification Logic: Reasoning with Reasons, Cambridge University Press, 2019.
Miércoles 20 de septiembre, 16:00 ~ 16:20
Semántica de las $F_{1}$-estructuras para los cálculos paraconsistentes $C_{n}$, $n\ge 2$
Andrea Carina Murciano
Instituto de Ciencias Básicas - Área Matemática. Facultad de Filosofía, Humanidades y Artes. Universidad Nacional de San Juan, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
En este trabajo definimos valuaciones que constituyen semánticas para los cálculos paraconsistentes $C_{n}$, $n \geq 2$. Estas lógicas fueron introducidas por Newton C. A. da Costa en [1] y, actualmente, se consideran casos particulares de las LFIs.
Nuestro estudio se centra en la correctitud, completitud y decidibilidad de esta semántica, la cual se basa en una interpretación para $C_{1}$ sobre modelos algebraicos-relacionales, denominados "$F_{1}$-estructuras" ([3], [4]). Además, presentamos ciertas extensiones booleanas que sirven como herramientas para realizar comparaciones con la semántica planteada en [2].
Trabajo en conjunto con: Carla N. Naccarato (Universidad Nacional de San Juan, Argentina), Gabriela Eisenberg (Universidad Nacional de San Juan, Argentina) y Verónica A. Quiroga (Universidad Nacional de San Juan, Argentina).
Referencias
[1] DA COSTA, N. C. A. Sistemas Formais Inconsistentes. UFPR, Curitiba, 1993.
[2] LOPARIC, A., AND ALVES, E. H. The semantics of the systems $C_n$ of da Costa. In Proceedings of the Third Brazilian Conference on Mathematical Logic (São Paulo, 1980), A. I. Arruda, N. C. A. da Costa, and A. M. Sette, Eds., Sociedade Brasileira de Lógica, pp. 119–129.
[3] QUIROGA, V. An alternative definition of $F$-structures for the logic $C_1$. Bulletin of the Section of Logic 42, 3/4 (2013), 119–134.
[4] QUIROGA, V. A. Estudio de un modelo algebraico-relacional para $C_1$ y $CILA$. PhD thesis, Universidad Nacional de San Luis, 2022.
Miércoles 20 de septiembre, 16:20 ~ 16:40
Productos twist y rotaciones
Miguel Andrés Marcos
FIQ, CONICET - UNL, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
Las lógicas subestructurales son sistemas lógicos que enmarcan dentro de una misma teoría lógicas que fueron surgiendo por diversos motivos y con diferentes metodologías. Los modelos algebraicos que mejor se adecúan a la gran mayoría de estos sistemas son los retículos residuados.
En este trabajo compararemos dos construcciones de retículos residuados: por un lado las rotaciones y por el otro los productos twist. Ambas construcciones así como las variedades que generan permiten que se pueda estudiar retículos residuados en términos de otros, por lo general más simples.
Las rotaciones conexas y disconexas así como sus generalizaciones [7, 6, 4] proporcionan una forma de obtener un nuevo retículo residuado a partir de otro `rotando' una subestructura del mismo. Las álgebras pertenecientes a variedades generadas por estas rotaciones podrán ser estudiadas a partir de subestructuras de las mismas, dadas por la categoría de `tripletes' de [4].
Por otro lado los productos twist [8, 9, 1, 2, 3], al tener como reducto el producto de un retículo y su orden-dual, pueden pensarse como un tipo distinto de rotación, que en general no es comparable con las antes mencionadas. Las álgebras pertenecientes a variedades generadas por productos twist se pueden estudiar a partir de la imagen del `conúcleo de Nelson' de [3].
Una comparación entre productos twist y rotaciones se hizo en [1], para el caso particular de retículos residuados de Nelson.
La generalización de la construcción twist presentada en [10,5] permite una nueva forma de comparación entre las rotaciones generalizadas presentadas en [4] y ciertos productos twist, así como también las variedades generadas por ambas clases. Las álgebras que pertenezcan a ambas clases podrán ser estudiadas tanto desde su representación por tripletes como por su representación twist, lo que permitirá una mayor comprensión de estos retículos residuados.
Trabajo en conjunto con: Manuela Busaniche (FIQ, CONICET - UNL, Argentina), Umberto Rivieccio (LHFC - UNED, Madrid, España) y Sara Ugolini (IIIA – CSIC, Barcelona, España).
Referencias
[1] M. Busaniche and R. Cignoli, Constructive logic with strong negation as a substructural logic, J. Log. Comput. 20 (2010), 761-793.
[2] M. Busaniche and R. Cignoli, The subvariety of commutative residuated lattices respresented by twist-products, Algebra Universalis 71 (2014) 5-22.
[3] M. Busaniche, N. Galatos and M. Marcos, Twist structures and Nelson conuclei, Stud Logica (2022).
[4] M. Busaniche, M. Marcos and S. Ugolini, Representation by triples of algebras with an MV-retract, Fuzzy Sets and Systems 369, 82-102, (2019).
[5] M. Busaniche and U. Rivieccio, Nelson conuclei and nuclei: the twist construction beyond involutivity. Manuscript.
[6] R. Cignoli and A. Torrens, Free Algebras in Varieties of Glivenko MTL-algebras Satisfying the Equation 2(x2)=(2x)2, Studia Logica 83, (2006) 157-181.
[7] S. Jenei, Structure of left-continuous triangular norms with strong induced negations. (I) Rotation construction, Journal of Applied Non-Classical Logics 10 (1), (2000) 83-92.
[8] J. Kalman, Lattices with involution, Trans. Amer. Math. Soc. 87 (1958), 485-491.
[9] D. Nelson, Constructible falsity, Journal of Symbolic Logic, 14:16-26, 1949.
[10] U. Rivieccio and M. Spinks, Quasi-Nelson algebras, Electronic Notes in Theoretical Computer Science, 344:169-188, 2019.
Jueves 21 de septiembre, 9:00 ~ 9:40
Introducción a los asistentes de pruebas basados en teoría de tipos dependientes, en específico "Coq'' (y resultados parciales sobre Redex $\rightarrow$ Coq)
Mallku Soldevila
FAMAF, Universidad Nacional de Córdoba, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
En esta comunicación comenzaremos recorriendo brevemente ideas que surgieron en la matemática durante la primera mitad del siglo pasado, y en términos de las cuales podemos justificar la implementación de un asistente de pruebas basado en teoría de tipos dependientes. Revisaremos conceptos de lógica intuicionista, lambda-cálculo y teoría de tipos, lo que nos permitirá entender las razones por las cuales podemos admitir (ciertos) programas en un lenguaje con tipos dependientes, como análogos computacionales de las pruebas que escribimos en papel.
A continuación introduciremos "Coq": un asistente de pruebas basado en teoría de tipos dependientes, ampliamente utilizado en esfuerzos de formalización de semántica de lenguajes de programación reales. Revisaremos construcciones fundamentales del "Cálculo de Construcciones Inductivas" (el lenguaje y semántica fundacional de Coq), mencionaremos sus propiedades teóricas principales, y estudiaremos ejemplos de definiciones de tipos inductivos, proposiciones y una demostración.
Finalmente comentaremos, de manera breve, sobre los primeros pasos dados en el desarrollo de una herramienta para automatizar la traducción de un modelo de semántica de reducciones en Redex, hacia un modelo (idealmente) semánticamente equivalente en Coq. La intención es proporcionar automatización a (algunas partes) de la certificación de propiedades fundamentales de tales modelos.
Trabajo en conjunto con: Dr. Beta Ziliani (FAMAF, UNC y Manas.Tech, Argentina).
Referencias
[1] Casey Klein, Jay McCarthy, Steven Jaconette, Robert Bruce Findler (2011) A semantics for context- sensitive reduction semantics. En: APLAS’11.
Jueves 21 de septiembre, 9:40 ~ 10:00
Generalizando el Framework de Katzuno y Mendelzon para AGM con un enfoque semántico
Daniel Grimaldi
Departamento de Computación, FCEyN-UBA, e Instituto de Ciencias de la Computación (UBA-CONICET), Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
Hay muchas maneras de modelar cómo una agente revisa sus creencias para incorporar nueva información, no sólo mediante la modelización de sus cambios de creencias, sino también considerando cómo se representa ese conocimiento. En el modelo más extendido, el modelo AGM [1], el conocimiento de la agente está fijado y se denota como un conjunto de fórmulas cerrado por consecuencia lógica, conocido como conjunto de creencias (belief set), y la nueva información es una fórmula en el lenguaje que actúa como un parámetro, pero hay muchas otras opciones.
En [2] Katsuno y Mendelzon (KM) adaptaron el modelo AGM para un lenguaje proposicional finito L, pero donde el conocimiento original y la nueva información están representados homogéneamente en el siguiente sentido: (1) ambos se representan de la misma manera, reescribiendo los conjuntos de creencias como fórmulas usando que L es finito; (2) el conocimiento original de la agente no es un valor fijo, sino un parámetro de la misma manera que la nueva información. En este contexto, los autores caracterizaron los operadores clásicos de AGM en términos de interpretaciones, también conocidos como la representación de mundos posibles.
Esta representación homogénea rara vez se ve, principalmente debido a la tradición de modelar a la agente como aquella que tiene un conocimiento y la capacidad de decidir cómo cambiarlo al recibir nueva información. En KM esta concepción cambia: lo que se tiene son pares de información con los que la agente tiene que lidiar, pero el papel de la agente es simplemente decidir qué hacer con ellos.
Nuestra propuesta es generalizar lo planteado en [2] para un contexto infinitario, conservando esta representación homogénea. Es decir, por un lado recuperamos la representación del conocimiento original como un conjunto de creencias, pero también escribimos de esta manera a la nueva información. Al hacer esto, mantenemos simultáneamente el contexto infinitario del AGM clásico y ambas piezas de conocimiento tienen el mismo tipo de representación. Y por otro lado, consideramos el conocimiento original como un parámetro. Todo esto lo desarrollamos desde la representación de mundos posibles para luego adaptarlo a diferentes contextos.
Creemos que esta generalización que parte de la representación de mundos posibles se puede aplicar a cualquier operador definido dentro del esquema KM de manera intuitiva, introduciéndolos en principio como operadores de cambio múltiple restringidos a conjuntos de creencias. Aquí sólo presentamos cómo hacerlo para operadores de revisión y contracción y probamos las identidades de Levi y Harper, no sólo porque muchos otros operadores se definen a partir de ellos, sino también porque hay conexiones interesantes con operadores conocidos de cambio múltiple [3] [4].
Trabajo en conjunto con: M. Vanina Martinez (Instituto de Investigación en Inteligencia Artificial, Barcelona, España) y Ricardo O. Rodriguez (Departamento de Computación, FCEyN-UBA, e Instituto de Ciencias de la Computación, UBA-CONICET, Argentina).
Referencias
[1] Alchourrón, C. E. y Gärdenfors, P. y Makinson, D., ``On the logic of theory change: Partial meet contraction and revision functions", The Journal of Symbolic Logic (1985), Vol. 3, pp. 510-530.
[2] Katsuno, H. y Mendelzon, A., ``Propositional knowledge base revision and minimal change", Technical Report nº3, Department of Computer Science, University of Toronto (1991).
[3] Fuhrmann, A. y Hansson, S. O., ``A Survey of Multiple Contractions", Journal of Logic, Language, and Information (1994), Vol. 3, No. 1, pp. 39-75.
[4] Hansson, S.O., ``Reversing the Levi identity", Journal of Philosophical Logic (1993), Vol. 22, pp. 637–669.
Jueves 21 de septiembre, 10:30 ~ 10:50
A Topological Study of $k$-rough Heyting Algebras
Florencia Valverde
Instituto de Ciencias Básicas, Universidad Nacional de San Juan, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
The theory of rough sets has been the subject of nearly two decades of research in both foundations and various applications (see [1]). A substantial portion of the work done on the theory has been devoted to studying its algebraic aspects (see [2]). Specific algebraic structures, such as approximate algebras and rough lattices, have been developed to represent rough sets. These algebraic structures provide a mathematical framework for the analysis and application of rough sets in various fields. In summary, the study of the algebraic aspects of rough sets has played a significant role in the conducted research in this field. It has led to the development of tools and techniques for analyzing and applying rough sets in diverse areas. In particular, Eric San Juan introduced the notion of $k$-rough Heyting algebras as an algebraic formalism for reasoning about increasing finite sequences in Boolean algebras in general and generalizations of rough set concepts in particular in his work (see [3]). The main objective of this work is to conduct a topological study of $k$-rough Heyting algebras.
Trabajo en conjunto con: Federico Almiñana (Universidad Nacional de San Juan, Argentina) y Gustavo Pelaitay (Universidad Nacional de San Juan, Argentina).
Referencias
[1] S. Comer. An algebraic approach to the approximation of information. Fundamenta Informaticae 14 (1991), 492– 502.
[2] Pawlak, Z. Rough sets. International Journal of Computer and Information Sciences 11 (1982), 341-356.
[3] E. San Juan, Heyting algebras with Boolean operators for rough sets and information retrieval applications. Discrete Applied Mathematics 156 (2008), 967–983.
Jueves 21 de septiembre, 10:50 ~ 11:10
Characterization of Subdirectly Irreducible Heyting Algebras with Negative Tense Operators
Gustavo Pelaitay
Instituto de Ciencias Básicas, Universidad Nacional de San Juan y CONICET, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
In this research work, a comprehensive study of Heyting algebras with four negative tense operators: $g$, $h$, $f$, and $p$, has been conducted. The main objective has been to provide a proof that these algebras offer a suitable algebraic semantics for intuitionistic propositional logic with negative Galois connections [1]. The analysis has been centered on characterizing subdirectly irreducible algebras within this new variety of Heyting algebras. To achieve this, Hasimoto's results [2] have been utilized to provide an algebraic characterization.
Trabajo en conjunto con: Federico Almiñana (Universidad Nacional de San Juan) y William Zuluaga (Universidad Nacional del Centro de la Provincia de Buenos Aires).
Referencias
[1] Ma, M., Li, G. Intuitionistic Propositional Logic with Galois Negations. Stud Logica 111, 21–56 (2023).
[2] Hasimoto, Y., Heyting algebras with operators, Mathematical Logic Quarterly 47(2):187-196, 2001.
Jueves 21 de septiembre, 11:10 ~ 11:30
Ordenes subyacentes a bandas regulares a derecha
Joel Kuperman
Universidad Nacional de Córdoba, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
La variedad de las bandas (semigrupos idempotentes) y sus subvariedades han sido estudiadas por Gerhard en [1]. La ecuación $x\cdot y=x$ determina un preorden sobre las álgebras de esta variedad y es un orden parcial si y solo si dicha variedad satisface la ecuación $x\cdot y\cdot x=y\cdot x$. Las álgebras de dicha variedad se conocen como `bandas regulares a derecha'.
$\mathbf{\rm Afirmación{:}}$ Si $A$ es una banda regular a derecha, entonces la relación $\theta:=\{(x,y)\in A^2: x\cdot y=y\ \& \ y\cdot x=x\}$ es una congruencia sobre $A$ y $A/\theta$ es un semirretículo.
Tenemos entonces que los semirretículos constituyen una subvariedad de las bandas regulares a derecha. El orden parcial asociado a aquellos es bien entendido, pero no sucede lo mismo en otras subvariedades ([2]). Consideremos la subvariedad de las bandas que satisfacen la identidad $x\cdot y\cdot z=y\cdot x\cdot z$. Denominamos `posets normales' a los órdenes asociados a álgebras de esta subvariedad. Presentaremos un resultado que caracteriza a los posets normales:
$\mathbf{\rm Teorema{:}}$ Sea $P$ un poset. $P$ es normal si y solo si existen un semirretículo inferior $S$ y un homomorfismo $f:P\rightarrow S$ que cumple que $f|_{p{\downarrow}}$ es un isomorfismo entre $p{\downarrow}$ y $f(p){\downarrow}$ para todo ${p\in P}$.
Trabajo en conjunto con: Pedro Sánchez Terraf (Universidad Nacional de Córdoba, Argentina) y Alejandro Petrovich (Universidad Nacional de Buenos Aires, Argentina).
Referencias
[1] Gerhard, J. A. (1970), The lattice of equational classes of idempotent semigroup, Journal of Algebra, 15 (2): 195–224.
[2] Kuperman, J. (2022), Estudios sobre posets asociativo, Trabajo especial de la Licenciatura en Matemática, UNC.