Algoritmos para decidir definibilidad de relaciones en fragmentos de primer orden

Abstract

En este trabajo desarrollamos algoritmos para decidir definibilidad de relaciones sobre familias finitas de estructuras finitas de primer orden. Presentamos algoritmos para los siguientes tipos de fórmulas: abiertas, abiertas positivas, existenciales, existenciales positivas y fórmulas sin restricciones. El punto de partida para estos algoritmos es una serie de resultados teóricos que caracterizan la definibilidad en términos de la preservación de morfismos. Presentamos además procedimientos para generar las álgebras de relaciones definibles en los formatos arriba enumerados. Adicionalmente, introducimos el paquete Definability desarrollado para SageMath, en el cual se implementan los algoritmos desarrollados. Las pruebas de este paquete inspiraron un teorema que caracteriza las relaciones binarias definibles por existenciales positivas en reticulados distributivos.

In this work we develop algorithms to decide definability of relations over finite families of finite first order structures. We present algorithms for the following kinds of formulas: open, positive open, existential, positive existential and without restrictions. The starting point to these algorithms is a series of theoretical results characterizing definability in terms of preservation of morphisms. We also present procedures to generate the algebras of defi nable relations for each of the above listed formats. Additionally, we introduce a package for SageMath, Definability, where the algorithms are implemented. The testing of this package inspired a theorem characterizing the binary relations definable by positive existential formulas over distributive lattices.