Delta-árboles de implicantes e implicados y reducciones de lógicas en ATPS

Abstract

EL trabajo pertenece al campo de la demostración automática para las lógicas multivaluadas, tarea que se aborda desde el estudio de la satisfacibilidad en lógicas signadas, Una de las aportaciones de la tesis es la introducción de las lógicas signadas con dos enriquecimientos respecto de otras aproximaciones: se consideran más conectivos y se abre la sensibilidad de que las lógicas sean reducidas. La relación entre las lógicas multivaluadas y las lógicas signadas se establece con las transformaciones de signado; en la tesis se estudia la eficiencia de estas transformaciones y se describe una familia (que amplia las existentes en la bibliografía) de lógicas signables, es decir, que admiten una transformación de signado eficiente. Para el resto de las lógicas se propone una técnica alternativa: el signado perezoso, aplicable a demostradores basados en simplificaciones. En la segunda parte de la tesis construyen dos algoritmos de satisfacibilidad para lógicas signadas dentro de la metodología TAS. Estos algoritmos se describen mediante reducciones, transformaciones que disminuyen el tamaño, tanto de la fórmula como de la lógica, antes de aplicar los procesos de ramificación culpables de la complejidad exponencial de estos algoritmos. Estas transformaciones hacen uso de la información que se obtiene a partir de los implicantes e implicados de las subfórmulas de la una fórmula dada. En el segundo demostrador se utiliza una nueva representación de las fórmulas signadas, los a-árboles, para mejorar las transformaciones y reducir su coste computacional, debido a que se utilizan justamente los implicantes/implicados para describir la representación.