Técnicas de razonamiento automático para lógicas híbridas

Mostrar todas las versiones(3)

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, s...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Gorín, Daniel Alejandro
Formato:	Tesis Doctoral
Lenguaje:	Inglés
Publicado:	2009
Materias:	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
Acceso en línea:	https://hdl.handle.net/20.500.12110/tesis_n4583_Gorin
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:tesis_n4583_Gorin
record_format	dspace
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language	Inglés
orig_language_str_mv	Inglés
topic	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
spellingShingle	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 Gorín, Daniel Alejandro Técnicas de razonamiento automático para lógicas híbridas
topic_facet	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
description	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.
format	Tesis Doctoral
author	Gorín, Daniel Alejandro
author_facet	Gorín, Daniel Alejandro
author_sort	Gorín, Daniel Alejandro
title	Técnicas de razonamiento automático para lógicas híbridas
title_short	Técnicas de razonamiento automático para lógicas híbridas
title_full	Técnicas de razonamiento automático para lógicas híbridas
title_fullStr	Técnicas de razonamiento automático para lógicas híbridas
title_full_unstemmed	Técnicas de razonamiento automático para lógicas híbridas
title_sort	técnicas de razonamiento automático para lógicas híbridas
publishDate	2009
url	https://hdl.handle.net/20.500.12110/tesis_n4583_Gorin
work_keys_str_mv	AT gorindanielalejandro tecnicasderazonamientoautomaticoparalogicashibridas AT gorindanielalejandro automatedreasoningtechniquesforhybridlogics
_version_	1782027111900381184
spelling	todo:tesis_n4583_Gorin2023-10-03T12:48:42Z Técnicas de razonamiento automático para lógicas híbridas Automated reasoning techniques for hybrid logics Gorín, Daniel Alejandro 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 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. Hybrid logics augment classical modal logics with machinery for describing and reasoning about identity, which is crucial in many settings. Although modal logics we would today call "hybrid" can be traced back to the work of Prior in the 1960's, their systematic study only began in the late 1990's. Part of their interest comes from the fact they fill an important expressivity gap in modal logics. In fact, they are sometimes referred to as "modal logics with equality". One of the unifying themes of this thesis is the satisfiability problem for the arguably best-known hybrid logic, H(@; !), and some of its sublogics. Satisfiability is the basic problem in automated reasoning. In the case of hybrid logics it has been studied fundamentally using the tableaux method. In this thesis we attempt to complete the picture by investigating satisfiability for hybrid logics using first-order resolution (via translations) and variations of a resolution calculus that operates directly on hybrid formulas. We present firstly several satisfiability-preserving, linear-time translations from H(@; !) to first-order logic. These are conceived in a way such that they tend to reduce the search space of a resolution-based theorem prover for first-order logic. notations can be safely ignored. We then move our attention to resolution-based calculi that work directly on hybrid formulas. In particular, we will consider the so-called direct resolution calculus. Inspired by first-order logic resolution, we turn this calculus into a calculus of ordered resolution with selection functions and prove that it possesses the reduction property for counterexamples from which it follows its completeness and that it is compatible with the well-known standard redundancy criterion. We also show that certain refinement of this calculus constitutes a decision procedure for H(@), a decidable fragment of H(@; !). In the last part of this thesis we investigate certain normal forms for hybrid logics and other extended modal logics. We are interested in normal forms where certain modalities can be guaranteed not to occur under the scope of other modal operators. We will see that these kind of transformations can be exploited in a pre-processing step in order to reduce the number of inferences required by a modal prover. In an attempt to formulate these results in a way that encompasses also other extended modal logics, we arrived at a formulation of modal semantics in terms of a novel type of models that are coinductively defined. Many extended modal logics (such as hybrid logics) can be defined in terms of classes of coinductive models. This way, results that had to be proved separately for each difierent language (but whose proofs were known to be mere routine) now can be proved in a general way. Fil: Gorín, Daniel Alejandro. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2009 Tesis Doctoral PDF Inglés info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n4583_Gorin

Técnicas de razonamiento automático para lógicas híbridas

Ejemplares similares