Resolución SL*: Un paradigma basado en resolución lineal para la demostración automática

Abstract

El trabajo incluido en la presente tesis se enmarca dentro del campo de la demostración automática de teoremas y consiste en la estudio, definición y desarrollo de un paradigma de resolución lineal, denominado Resolución SL*. La razón para utilizar la denominación de paradigma reside en el hecho de que en sí misma resolución SL* no es un procedimiento, sino que se puede entender como una forma de razonamiento con ciertos parámetros cuya instanciación da lugar a diferentes procedimientos que son adecuados para el tratamiento de distintos tipos de problemas. Por otro lado, se le ha dado el nombre de resolución SL* porque, como posteriormente se explicará, está muy cercano a Eliminación de Modelos y a resolución SL (de ahí la primera parte del nombre). El asterisco final quiere denotar su parametrización, de forma que los procedimientos instancias de resolución SL* serán denominados con una letra más en vez del asterisco, como posteriormente se verá. La tesis ha sido dividida en cuatro capítulos que se describen brevemente a continuación. En el primero se realiza una breve introducción histórica a la demostración automática, que va desde los orígenes de la lógica con el uso de las primeras notaciones matemáticas formales en el siglo XVI hasta la aparición de los resultados más importantes de la lógica descubiertos por Herbrand, Gödel, Church, etc. Se hace un especial hincapié en este capítulo en la demostración automática realizando un recorrido desde sus orígenes a finales del siglo XVIII hasta el momento actual, en el cual es posible ver cuál ha sido la evolución de este campo y qué descubrimientos y resultados se pueden presentar como los principales puntos de inflexión. En el segundo capítulo se presentan la resolución lineal y algunos de sus principales refinamientos, ya que resolución SL* es un variación de resolución SL y por tanto de resolución lineal. Para ello se introduce el principio de resolución, viendo los problemas de su mecanización, y posteriormente se ven dos refinamientos de resolución: resolución semántica y resolución lineal. Para concluir se estudian los principales refinamientos de resolución lineal: resolución de entrada, resolución lineal con fusión, resolución lineal con subsumción, resolución lineal ordenada, resolución MTOSS y TOSS, Eliminación de Modelos, resolución SL y el sistema MESON. En el tercer capítulo se presentan y estudian con profundidad las principales aportaciones al campo de la demostración automática que se han producido en los últimos años y que están cercanas a la aproximación del presente trabajo. Se han incluido los siguientes trabajos: el demostrador PTTP de Stickel, el sistema MESON basado en secuencias de Plaisted, el demostrador SATCHMO de Manthey y Bry, los procedimientos Near-Horn Prolog de Loveland y otros autores y, por último, el demostrador SETHEO de Bibel y otros autores. Obviamente no se han incluido todos los demostradores y procedimientos, pero sí aquellos que se han considerado como los más interesantes y cercanos a resolución SL* de manera que sea posible realizar comparaciones, de forma que queden patentes las aportaciones realizadas. En el cuarto capítulo se presenta resolución SL*. Se da la definición formal de la misma y se introduce el concepto fundamental de elección de ancestros. La elección de ancestros es el mecanismo que permite controlar la aplicación de la resolución de ancestro haciendo posible una reducción del coste de su aplicación y una adecuación de resolución SL* al tipo de problema a tratar. Posteriormente se ven las principales instancias de resolución SL*, los procedimientos SLT y SLP. En este capítulo se hace un especial hincapié en la elección de ancestros, ya que es la principal aportación de resolución SL*, analizando tanto las ventajas que aporta asociadas al incremento de la eficiencia como el hecho de dotar a resolución SL* la capacidad de adaptarse a los problemas que trata. También en este capítulo se presenta una implementación de resolución SL*, en particular del procedimiento SLT, y se incluyen resultados sobre un conjunto extenso de problemas del campo de la demostración automática. En la última sección de este capítulo se realiza una comparación de resolución SL* con los demostradores y sistemas más cercanos, tanto a nivel de características como de resultados.