CALCULO PROPOSICIONAL

Autor: MARTÍN MATEOS FRANCISCO JESÚS.
Año: 2001.
Universidad: SEVILLA.
Centro de lectura: ESCUELA SUPERIOR DE INGENIEROS.
Centro de realización: E.T.S. DE INGENIERÍA INFORMÁTICA.

Resumen: En este trabajo se desarrolla una formalización de sistemas de razonamiento proposicionales y se verifican automáticamente sus principales propiedades en el sistema de demostración automática ACL2. También se analizan las características comunes a determinados cálculos bien conocidos, definiendo un marco genérico del que son casos particulares. El trabajo comienza con la formalización de la lógica proposicional, para la que se consideran dos semánticas, la clásica y la semántica trivalorada fuerte de Kleene. Una vez hecho esto, se desarrollan procedimientos de decisión de satisfacibilidad, validez y consecuencia lógica (tanto en la semántcia clásica como en la de Kleene) basados en el cálculo de los tableros semánticos y el cálculo de secuentes. Se proporcionan implementaciones verificadas de estos procedimientos. A partir de estos dos métodos de decisión de satisfacibilidad se define un marco genérico que abstrae sus características comunes: los Sistemas de Transformación Proposicionales. Esta abstracción permite desarrollar procedimientos de decisión de satisfacibilidad a partir de un conjunto de reglas de transformación con determinadas propiedades básicas. La implementación del marco genérico se puede instanciar para construir de forma automática procedimientos verificados de decisión de satisfacibilidad. Se muestra cómo se realiza esta instancia para los métodos basados en tableros semánticos y en secuentes. El desarrollo del marco genérico se ha realizado tanto para la semántica clásica como para la semántcia de Kleene. A continuación se estudian otros procedimientos de decisión de satisfacibilidad, analizando la posibilidad de expresarlos como sistemas de transformación proposicionales. Esto ocurre con el procedimiento de Davis y Putnam, el cual es desarrollado primero de forma independiente al marco genérico y después se expresa como una instancia del mismo. Este desarrollo se realiza tanto para la semántica clásica como para la de Kleene. Se proporciona una implementación genérica de este procedimiento, en el sentido de que depende de una función de selección caracterizada por un conjunto de propiedades. Esta función proporciona la posibilidad de incorporar heurísticas que mejoran el método. Un ejemplo de esta técnica es presentado al desarrollar el método de Davis y Putnam como un procedimiento obtenido al considerar una función de selección concreta en un procedimiento de decisión basado únicamente en la regla de bifurcación por un literal. Finalmente se analiza el método de resolución con algunas de sus variantes (resolución positiva, negativa, semántica, …). Este método no tiene las características adecuadas que permiten expresarlo como un sistema de transformación proposicional. Su desarrollo también se hace de forma genérica, haciendo depender los pasos de resolución de una propiedad de las cláusulas padre, de forma que las variantes citadas se pueden expresar como instancias. La formalización obtenida se instancia para generar procedimientos verificados que implementan las variantes citadas de resolución. La prueba de la completitud de este método de resolución genérico es la presentada por Bezem en su artículo "Completeness of resolution revisited" y es la primera automatización que se realiza de la misma.

Autor: MAÑA SERRES FELIP.
Año: 1996.
Universidad: AUTONOMA DE BARCELONA.
Centro de lectura: CIENCIAS.
Centro de realización: DEPARTAMENTO: INFORMATICA PROGRAMA DE DOCTORADO: GRAFICOS, IMAGENES DIGITALES E INTELIGENCIA ARTIFICIAL .

Resumen: EN ESTA TESIS SE PRESENTAN PROCEDIMIENTOS DE PRUEBA PARA LOGICAS PROPOSICIONALES MULTIVALUADAS. SE DEFINEN CALCULOS COMPLETOS, ESTRUCTURAS DE DATOS EFICIENTES, HEURISTICAS PARA CONTROLAR EL ESPACIO DE BUSQUEDA Y TECNICAS PARA AHORRAR CALCULOS NO NECESARIOS. EN PRIMER LUGAR, SE DISEÑAN ALGORITMOS PARA COMPROBAR LA SATISFACTIBILIDAD DE FORMULAS SIGNADAS (GENERALES Y REGULARES), LOS CUALES SIRVEN PARA RESOLVER EL PROBLEMA DE LA SATISFACTIBILIDAD EN CUALQUIER LOGICA FINITAMENTE-VALUADA. LUEGO, SE DEMUESTRA QUE EL PROBLEMA DE LA SATISFACTIBILIDAD DE FORMULAS HORN REGULARES TIENE UNA COMPLEJIDAD LINEAL, Y QUE EL PROBLEMA DE LA 2-SATISFACTIBILIDAD PARA FORMULAS SIGNADAS ARBITRARIAS ES NP-COMPLETO, AUNQUE ADMITE SOLUCIONES POLINOMILES SI LAS FORMULAS SON REGULARES O LOS SIGNOS SON SINGLETONS. FINALMENTE, SE DISEÑA UN INTERPRETE LINEAL PARA UNA AMPLIA FAMILIA DE LOGICAS INFINITAMENTE-VALUADAS, EL CUAL ESTA BASADO EN UNA REGLA DE INFERENCIA MODUS-PONENS E INCORPORA UNA REGLA DE NEGACION POR FALLO FINITO MULTIVALUADA Y UN OPERADOR DE CORTE MULTIVALUADO.

Autor: GARCIA LAPRESTA JOSE LUIS.
Año: 1990.
Universidad: BARCELONA.
Centro de lectura: MATEMATICAS.
Centro de realización: DEPARTAMENTO: LOGICA, HISTORIA I FILOSOFIA DE LA CIENCIA PROGRAMA DE DOCTORADO: LOGICA MATEMATICA.

Resumen: SE HAN ESTUDIADO LOGICAS ABSTRACTAS QUE CUMPLEN EL TEOREMA DE DEDUCCION CON RESTRICCIONES EN EL CARDINAL DEL CONJUNTO DE PREMISAS. EL ESTUDIO DE ESTAS LOGICAS, AQUI LLAMADAS "FINITAMENTE DEDUCTIVAS" SE HA HECHO EN EL MARCO DE LA TEORIA DE LOGICAS ABSTRACTAS DE BROWN Y SUSZICO. HAN SIDO CARACTERIZADAS MEDIANTE VARIAS CLASES DE ALGEBRAS IMPLICATIVAS. ADEMAS, SE HAN INTRODUCIDO VARIOS CALCULOS PROPOSICIONALES ESTILO HILBERT RELACIONADOS CON LAS CLASES DE ALGEBRAS ESTUDIADAS. PARA PROPORCIONAR EJEMPLOS DE CALCULOS CUYAS LOGICAS PROPOSICIONALES FUERAN FINITAMENTE DEDUCTIVAS HA SIDO NECESARIO CONSIDERAR CALCULOS DE SECUENTES.

Autor: TIÑENA SALVAÑA FRANCESC.
Año: 1986.
Universidad: POLITECNICA DE CATALUÑA.
Centro de lectura: INFORMATICA.
Centro de realización: FACULTAT D INFORMATICA REPRESENTACIO DE LES ALGEBRES DE WAJSBER PER PRODUCTES.

Resumen: A TRAVES DE PRODUCTOS SUBDIRECTOS GLOBALES. REALIZAMOS TODA W-ALGEBRA COMO PRODUCTO SUBDIRECTO GLOBAL DE W-ALGEBRAS LOCALES SOBRE UN ESPACIO COMPACTO. DEFINIMOS Y ESTUDIAMOS CON ESPECIAL ENFASIS LAS W-ALGEBRAS QUE LLAMAMOS PROYECTABLES. REALIZAMOS TODA W-ALGEBRA PROYECTABLE COMO PRODUCTO BOCLEANO DE W-ALGEBRAS LINEALES. SE ESTUDIAN TAMBIEN LAS W-ALGEBRAS QUE LLAMAMOS DEBILMENTE PROYECTABLES Y FUERTEMENTE PROYECTABLES. FEFORMULAMOS LOS ANTERIORES RESULTADOS DESDE EL PUNTO DE VISTA DE LA TEORIA DE HACES . DAMOS UN EJEMPLO DE W-ALGEBRA QUE CONSISTE EN EL SEGMENTO DE UN GRUPO RETICULADO Y A CONTINUACION BASANDONOS EN UN TEOREMA NUESTRO DEMOSTRAMOS QUE TODA W-ALGEBRA PROYECTABLE SE PUEDE REALIZAR COMO EL SEGMENTO DE UN GRUPO RETICULADO CARTESIANO CON UNIDAD FUERTE U 0 Y PROYECTABLE COMO GRUPO RETICULADO.

Autor: RODRIGUEZ SALAS ANTONIO JESUS.
Año: 1980.
Universidad: BARCELONA.
Centro de lectura: MATEMATICAS.
Centro de realización: FACULTAD DE MATEMATICAS DE LA UNIVERSIDAD CENTRAL DE BARCELONA.

Resumen: TRAS UNA BREVE PRESENTACION DE LAS ALGEBRAS DE SALES ASOCIADAS A LA PARTE IMPLICATIVA DEL CALCULO PROPOSICIONAL INFINITO VALENTE DE LUKASIEWICZ SE ESTUDIAN LAS PROPIEDADES LOGICO-ALGEBRAICAS MAS IMPORTANTES DE LAS ALGEBRAS DE WAJSBERG PONIENDO ESPECIAL INTERES EN EL ESTUDIO DE LA SEMISIMPLICIDAD ARQUIMEDIANIDAD Y N+1- ACOTACION. CON RESPECTO A LOS CALCULOS N+1- VALENTES SE DEMUESTRA LA FINITUD DE LAS ALGEBRAS FINITAMENTE GENERADAS Y SE CALCULA SU CARDINAL PARA EL CASO DE LAS LIBRES.