Catálogo de publicaciones - tesis
Título de Acceso Abierto
Técnicas de razonamiento automático para lógicas híbridas
Daniel Alejandro Gorín Carlos Eduardo Areces Verónica Becher
publishedVersion.
Resumen/Descripción – provisto por el repositorio digital
Las "lógicas híbridas" extienden a las lógicas modales tradicionales con el poder de describir y razonar sobre cuestiones de identidad, lo cual es clave para muchas aplicaciones. Aunque lógicas modales que hoy llamaríamos "híbridas" pueden rastrearse hasta cuatro décadas atrás, su estudio sistem ático data de fines de la década del '90. Parte de su interés proviene de que llenan un hueco de expresividad importante de las lógicas modales tradicionales. Uno de los temas de esta tesis es el problema de la satisfacibilidad para la lógica híbrida más conocida, denominada H(@;!), y algunas de sus sublógicas. El de la satisfacibilidad es el problema fundamental en razonamiento automático. En el caso de las lógicas híbridas, éste se ha estudiado fundamentalmente a partir del método de tableaux. En esta tesis intentamos completar el panorama del área investigando el problema de la satisfacibilidad para lógicas híbridas usando resolución clásica de primer orden (vía traducciones) y variaciones de un cálculo basado en resolución que opera directamente sobre fórmulas híbridas. Presentamos, en primer lugar, traducciones de complejidad lineal de fórmulas de H(@;!) a lógica de primer orden, que preservan satisfacibilidad. Éstas están concebidas de manera de reducir el espacio de búsqueda de un demostrador automático basado en resolución de primer orden. Luego cambiamos nuestra atención a cálculos que operan directamente sobre fórmulas híbridas. En particular, consideramos el cálculo llamado de"resolución directa". Inspirados por el caso clásico, transformamos este cálculo en uno de resolución ordenada con funciones de selección y probamos que posee la "propiedad de reducción de contraejemplos", de lo cual se deduce que es completo y compatible con el criterio de redundancia estándar. Mostramos también que un refinamiento de este cálculo es un método de decisión para la sublógica decidible H(@). En la última parte de esta tesis, consideramos ciertas formas normales para lógicas híbridas y otras lógicas modales extendidas. En particular nos interesan formas normales donde se garantice que ciertas modalidades no aparecen por debajo de otros operadores modales. Este tipo de transformaciones puede ser aprovechadas en una etapa de preprocesamiento a fin de reducir el número de inferencias requeridas por un demostrador modal. Al intentar expresar estos resultados de extractibilidad de una manera que comprenda también otras lógicas modales extendidas, llegamos a una formulación de la semántica modal basada en un tipo novedoso de modelos definidos de manera coinductiva. Muchas lógicas modales extendidas (incluyendo las lógicas híbridas) pueden verse en términos de clases de modelos coinductivos. De esta manera, resultados que antes debían probarse por separado para cada lenguaje (pero cuyas pruebas eran en general rutinarias) pueden establecerse de manera general.Palabras clave – provistas por el repositorio digital
LOGICAS HIBRIDAS; DEMOSTRACION AUTOMATICA; TRADUCCIONES A PRIMER ORDEN; RESOLUCION DIRECTA; METODOS DE DECISION; MODELOS COINDUCTIVOS; FORMAS NORMALES; EXTRACTABILIDAD DE MODALIDADES; HYBRID LOGICS; AUTOMATED REASONING; FIRST-ORDER TRANSLATIONS; DIRECT RESOLUTION; DECISION METHODS; COINDUCTIVE MODELS; NORMAL FORMS; EXTRACTABILITY OF MODALITIES
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No requiere | 2009 | Biblioteca Digital (FCEN-UBA) (SNRD) |
|
Información
Tipo de recurso:
tesis
Idiomas de la publicación
- español castellano
País de edición
Argentina
Fecha de publicación
2009
Información sobre licencias CC