Simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías

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.

Saved in:
Bibliographic Details
Main Author: Orbe, Alejandro Ezequiel
Other Authors: Areces, Carlos Eduardo
Format: doctoralThesis biblioteca
Language:spa
Published: 2014-03
Subjects:Lógica matemática, Deducción y prueba de teoremas, Lógica modal, Mathematical Logic, Deduction and Theorem Proving, Razonamiento automático, SMT,
Online Access:http://hdl.handle.net/11086/2844
Tags: Add Tag
No Tags, Be the first to tag this record!
id dig-unc-ar-11086-2844
record_format koha
spelling dig-unc-ar-11086-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. 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/
institution UNC AR
collection DSpace
country Argentina
countrycode AR
component Bibliográfico
access En linea
databasecode dig-unc-ar
tag biblioteca
region America del Sur
libraryname Biblioteca 'Ing. Agrónomo Moisés Farber' de la Facultad de Ciencias Agropecuarias
language spa
topic Lógica matemática
Deducción y prueba de teoremas
Lógica modal
Mathematical Logic
Deduction and Theorem Proving
Razonamiento automático
SMT
Lógica matemática
Deducción y prueba de teoremas
Lógica modal
Mathematical Logic
Deduction and Theorem Proving
Razonamiento automático
SMT
spellingShingle Lógica matemática
Deducción y prueba de teoremas
Lógica modal
Mathematical Logic
Deduction and Theorem Proving
Razonamiento automático
SMT
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
description Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2014.
author2 Areces, Carlos Eduardo
author_facet Areces, Carlos Eduardo
Orbe, Alejandro Ezequiel
format doctoralThesis
topic_facet Lógica matemática
Deducción y prueba de teoremas
Lógica modal
Mathematical Logic
Deduction and Theorem Proving
Razonamiento automático
SMT
author Orbe, Alejandro Ezequiel
author_sort Orbe, Alejandro Ezequiel
title 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_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_sort simetrías en razonamiento automático : el caso de las lógicas modales y satisfacibilidad módulo teorías
publishDate 2014-03
url http://hdl.handle.net/11086/2844
work_keys_str_mv AT orbealejandroezequiel simetriasenrazonamientoautomaticoelcasodelaslogicasmodalesysatisfacibilidadmoduloteorias
_version_ 1756008915931234304

Similar Items