Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías
Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2014.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | doctoralThesis |
| Language: | spa |
| Published: |
2016
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/2844 |
| _version_ | 1801214427865808896 |
|---|---|
| author | Orbe, Alejandro Ezequiel |
| author2 | Areces, Carlos Eduardo |
| author_facet | Areces, Carlos Eduardo Orbe, Alejandro Ezequiel |
| author_sort | Orbe, Alejandro Ezequiel |
| collection | Repositorio Digital Universitario |
| description | Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2014. |
| format | doctoralThesis |
| id | rdu-unc.2844 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2016 |
| record_format | dspace |
| spelling | rdu-unc.28442022-10-13T11:16:39Z Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías Orbe, Alejandro Ezequiel Areces, Carlos Eduardo Lógica matemática Deducción y prueba de teoremas Lógica modal Mathematical Logic Deduction and Theorem Proving Razonamiento automático SMT Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2014. Fil: Orbe, Alejandro Ezequiel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. En esta tesis investigamos el uso de simetrías en el contexto de lógicas modales y de satisfacibilidad módulo teorías (SMT). Desarrollamos el marco teórico para utilizar las simetrías de una fórmula modal utilizando el marco provisto por los modelos modales coinductivos. Luego definimos algoritmos de detección de simetrías para fórmulas modales. Finalmente, presentamos un cálculo de tableaux que incorpora un mecanismo de bloqueo basado en simetrías, llamado bloqueo simétrico. Para SMT, desarrollamos un algoritmo de detección que permite detectar simetrías de símbolos no interpretados en una fórmula SMT. The study of symmetries has received much attention during the last years in the automated reasoning community, especially in propositional satisfiability solving (SAT solving), as they can help in solving many hard problems. In automated reasoning, the presence of symmetries in a problem?s search space may increase the difficulty of finding a solution by forcing a search algorithm to explore symmetric subspaces that do not contain solutions. Intuitively, if a problem has symmetries and we are able to identify them, we might use them to reduce the difficulty of rea- soning by directing a search algorithm to look for solutions only in non-symmetric parts of the search space. In this thesis we investigate symmetries for modal logics and Satisfiability Modulo Theories (SMT). For modal logics, we develop the theoretical framework for the study of symmetries in modal logics by generalizing the notion of symmetries of propositional formulas in conjunctive normal form to modal formulas. We prove two key results for the basic modal logic: that symmetries of a basic modal formula partition the model space into equivalence classes such that each equivalence class contains only models or only non-models, and that symmetries can be used as an inference mechanism, and therefore, they can be used to strengthen existing reasoning mechanisms. Fil: Orbe, Alejandro Ezequiel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2016-07-27T14:42:56Z 2016-07-27T14:42:56Z 2014-03 doctoralThesis http://hdl.handle.net/11086/2844 spa Atribución-NoComercial-CompartirIgual 2.5 Argentina http://creativecommons.org/licenses/by-nc-sa/2.5/ar/ |
| spellingShingle | Lógica matemática Deducción y prueba de teoremas Lógica modal Mathematical Logic Deduction and Theorem Proving Razonamiento automático SMT Orbe, Alejandro Ezequiel Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías |
| title | Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías |
| title_full | Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías |
| title_fullStr | Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías |
| title_full_unstemmed | Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías |
| title_short | Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías |
| title_sort | simetrias en razonamiento automatico el caso de las logicas modales y satisfacibilidad modulo teorias |
| topic | Lógica matemática Deducción y prueba de teoremas Lógica modal Mathematical Logic Deduction and Theorem Proving Razonamiento automático SMT |
| url | http://hdl.handle.net/11086/2844 |
| work_keys_str_mv | AT orbealejandroezequiel simetriasenrazonamientoautomaticoelcasodelaslogicasmodalesysatisfacibilidadmoduloteorias |