Algoritmos para decidir definibilidad de fragmentos de lógica en primer orden
Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2023.
Main Author: | |
---|---|
Other Authors: | |
Format: | bachelorThesis |
Language: | spa |
Published: |
2023
|
Subjects: | |
Online Access: | http://hdl.handle.net/11086/548395 |
_version_ | 1801214052359208960 |
---|---|
author | Ventura, Pablo Gabriel |
author2 | Campercholi, Miguel Alejandro Carlos |
author_facet | Campercholi, Miguel Alejandro Carlos Ventura, Pablo Gabriel |
author_sort | Ventura, Pablo Gabriel |
collection | Repositorio Digital Universitario |
description | Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2023. |
format | bachelorThesis |
id | rdu-unc.548395 |
institution | Universidad Nacional de Cordoba |
language | spa |
publishDate | 2023 |
record_format | dspace |
spelling | rdu-unc.5483952023-08-31T13:17:38Z Algoritmos para decidir definibilidad de fragmentos de lógica en primer orden Ventura, Pablo Gabriel Campercholi, Miguel Alejandro Carlos Teoría de modelos finitos Definibilidad Relaciones Algoritmos Morfismos Fragmentos de primer orden Model theory Finite model theory Definability Relations Algorithms Morphisms First order fragments Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2023. Fil: Ventura, Pablo Gabriel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Dada una estructura A, decimos que un conjunto T es definible en primer orden sin cuantificadores si y solo si existe una fórmula sin cuantificadores φ tal queA ⊨φ(x) para todo x∈T, mientras que A ⊭φ(x) para todo x∈A\T. Esta tesis doctoral aborda la definibilidad de primer orden sin cuantificadores desde un enfoque computacional. Se han desarrollado algoritmos eficientes basados en propiedades semánticas de los modelos y se han implementado para su uso como asistentes de investigación. También se presenta un manual de uso para las herramientas y un conjunto de pruebas para comprobar su eficiencia empíricamente. Finalmente, se ha estudiado la complejidad de estos problemas de definibilidad y se han presentado resultados teóricos que establecen los límites de su eficiencia computacional. Given a structure A, we say that a set T is definable in first-order logic without quantifiers if and only if there exists a first-order formula φ without quantifiers such that A ⊨φ(x) for all x∈T, while A ⊭φ(x) for all x∈A\T. This doctoral thesis addresses first-order definability without quantifiers from a computational approach. Efficient algorithms based on semantic properties of models have been developed and implemented for use as research assistants. A usage manual for the tools and a set of tests to empirically verify their efficiency are also presented. Finally, the complexity of these definability problems has been studied and theoretical results establishing the limits of their computational efficiency have been presented. Fil: Ventura, Pablo Gabriel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2023-08-08T14:41:45Z 2023-08-08T14:41:45Z 2023-06-29 bachelorThesis http://hdl.handle.net/11086/548395 spa Attribution-NonCommercial-NoDerivatives 4.0 Internacional http://creativecommons.org/licenses/by-nc-nd/4.0/ |
spellingShingle | Teoría de modelos finitos Definibilidad Relaciones Algoritmos Morfismos Fragmentos de primer orden Model theory Finite model theory Definability Relations Algorithms Morphisms First order fragments Ventura, Pablo Gabriel Algoritmos para decidir definibilidad de fragmentos de lógica en primer orden |
title | Algoritmos para decidir definibilidad de fragmentos de lógica en primer orden |
title_full | Algoritmos para decidir definibilidad de fragmentos de lógica en primer orden |
title_fullStr | Algoritmos para decidir definibilidad de fragmentos de lógica en primer orden |
title_full_unstemmed | Algoritmos para decidir definibilidad de fragmentos de lógica en primer orden |
title_short | Algoritmos para decidir definibilidad de fragmentos de lógica en primer orden |
title_sort | algoritmos para decidir definibilidad de fragmentos de logica en primer orden |
topic | Teoría de modelos finitos Definibilidad Relaciones Algoritmos Morfismos Fragmentos de primer orden Model theory Finite model theory Definability Relations Algorithms Morphisms First order fragments |
url | http://hdl.handle.net/11086/548395 |
work_keys_str_mv | AT venturapablogabriel algoritmosparadecidirdefinibilidaddefragmentosdelogicaenprimerorden |