Algoritmos para decidir definibilidad en fragmentos de lógica de primer orden | Defensa de tesis del Doctorado en Ciencias de la Computación

Tribunal Especial

Titulares:

Dr. José Patricio DIAZ VARELA (Depto. de Matemática - UNS)

Dr. Miguel María PAGANO (FAMAF)

Dr. Raúl Alberto FERVARI (FAMAF)

Día: jueves 29 de junio de 2023

Horario: 16.00 horas

Lugar: Aula Magna – FAMAF

Resumen: Dada una lógica ℒ, el problema de ℒ-definibilidad para estructuras finitas toma como entrada una estructura finita A y una relación objetivo 𝑇 sobre el dominio de A, y determina si existe una fórmula de ℒ cuya interpretación en A coincide con 𝑇. En este trabajo presentamos algoritmos que resuelven el problema de definibilidad para fórmulas de primer orden sin cuantificador. Nuestros algoritmos aprovechan una caracterización semántica de la definibilidad abierta mediante isomorfismos internos, que es correcta y completa. Presentamos un algoritmo enfocado en estructuras relacionales y, luego, otros dos enfocados en álgebras. En particular, el segundo algoritmo para álgebras proporciona además una fórmula en caso positivo. El enfoque algebraico también incluye el diseño de un algoritmo que calcula el tipo de isomorfismo de una tupla en una estructura algebraica finita. Se presentan pruebas de corrección y completitud de los algoritmos, así como pruebas empíricas que evalúan su rendimiento. Además, definimos formalmente e investigamos la complejidad computacional del problema de definibilidad para fórmulas abiertas de primer orden (es decir, fórmulas de primer orden sin cuantificador) con igualdad. Demostramos que la complejidad de este problema para fórmulas abiertas de primer orden (definibilidad abierta, para abreviar) es coNP-completa.