Resumen de Resolución SL*: un paradigma basado en resolución lineal para la demostración automática
EL TRABAJO INCLUIDO EN LA PRESENTE TESIS SE ENMARCA DENTRO DEL CAMPO DE LA DEMOSTRACION AUTOMATICA DE TEOREMAS Y CONSISTE EN EL ESTUDIO, DEFINICION Y DESARROLLO DE UN PARADIGMA DE RESOLUCION LINEAL, DENOMINADO RESOLUCION SL*: LA RAZON PARA UTILIZAR LA DENOMINACION DE PARADIGMA RESIDE EN EL HECHO DE QUE EN SI MISMA RESOLUCION SL* NO ES UN PROCEDIMIENTO, SINO QUE SE PUEDE ENTENDER COMO UNA FORMA DE RAZONAMIENTO CON CIERTOS PARAMETROS CUYA INSTANCIACION DA LUGAR A DIFERENTES PROCEDIMIENTOS QUE SON ADECUADOS AL TRATAMIENTO DE DISTINTOS TIPOS DE PROBLEMAS, POR OTRO LADO, SE LE HA DADO EL NOMBRE DE RESOLUCION SL* PORQUE, COMO POSTERIORMENTE SE EXPLICARA, ESTA MUY CERCANO A ELIMINACION DE MODELOS Y A RESOLUCION SL (DE AHI LA PRIMERA PARTE DEL NOMBRE). EL ASTERISCO FINAL QUIERE DENOTAR SU PARAMETRIZACION, DE FORMA QUE LOS PROCEDIMIENTOS INSTANCIAS DE RESOLUCION SL* SERAN DENOMINADOS CON UNA LETRA MAS EN VEZ DEL ASTERISCO, COMO POSTERIORMENTE SE VERA.
EN RESOLUCION SL* SE INTRODUCE EL CONCEPTO FUNDAMENTAL DE "ELECCION DE ANCESTROS". LA ELECCION DE ANCESTROS ES EL MECANISMO QUE PERMITE CONTROLAR LA APLICACION DE LA RESOLUCION DE ANCESTRO HACIENDO POSIBLE UNA REDUCCION DEL COSTE DE SU PALICACION Y UNA ADECUACION DE RESOLUCION SL* AL TIPO DE PROBLEMAS A TRATAR. EL TRABAJO HACE ESPECIAL HINCAPIE EN LA IMPORTANCIA DE LA ELECCION DE ANCESTROS, YA QUE ES LA PRINCIPAL APORTACION DE RESOLUCION SL*, ANALIZANDO TANTO LAS VENTAJAS QUE APORTA ASOCIADAS AL INCREMENTO DE LA EFICIENCIA COMO EL HECHO DE DOTAR A RESOLUCION SL* LA CAPACIDAD DE ADAPTARSE A LOS PROBLEMAS QUE TRATA. TAMBIEN SE PRESENTA UNA IMPLEMENTACION DE RESOLUCION SL*, EN PARTICULAR DEL PROCEDIMIENTO SLT, Y SE INCLUYEN RESULTADOS SOBRE UN CONJUNTO EXTENSO DE PROBLEMAS DEL CAMPO DE LA DEMOSTRACION AUTOMATICA.
