Agregando polimorfismo a una lógica que identifica proposiciones isomorfas

Ficha técnica

Resumen

Tanto los sistemas de tipos como los sistemas de pruebas distinguen elementos que tienen diferente forma aunque tengan el mismo significado, como pueden ser las pruebas de las conjunciones AB y BA, por lo cual una prueba de una no constituye una prueba de la otra, a pesar de que se puede demostrar mediante la existencia de un isomorfismo que dichas proposiciones son equivalentes. Sistema I es un cálculo lambda simplemente tipado con pares, extendido con una teoría ecuacional obtenida a partir de los isomorfismos de tipos existentes entre los tipos simples con pares, de forma tal que las proposiciones con mismo significado son equivalentes. En este trabajo proponemos una extensión de Sistema I hacia polimorfismo, añadiendo al sistema de tipos el cuantificador universal y sus isomorfismos relacionados.

Publicaciones

Proyectos

Técnicas de Inteligencia Artificial Neuro-simbólica. Financiado por Comisión de Investigaciones Científicas y Facultad de Informática y Universidad Abierta Interamericana. Dirigido por Claudia Pons. CoDirigido por Roxana Giandini. Duración: 1/1/2019-31/12/2024

Técnicas y herramientas para ingeniería de software web adaptable y ágil basada en modelos con soporte semántico y de crowdsourcing. Financiado por Universidad Nacional de la Plata (Acreditado en el Programa de Inventivos). Dirigido por Antonelli, Ruben Leandro. CoDirigido por Urbieta, Mario Matias. Duración: 1/1/2020-31/12/2022

Desarrollo de herramientas inteligentes para la gestión y toma de decisiones en el ámbito de la ciencia abierta y ciudadana. Financiado por CICPBA. Dirigido por Claudia Pons. Duración: 1/7/2019-31/7/2021