TEORIA DE LA DEMOSTRACION

Autor: CORDERO ORTEGA PABLO JOSE.
Año: 1999.
Universidad: MALAGA.
Centro de lectura: INFORMATICA.
Centro de realización: E.T.S. I. INFORMATICA.

Resumen: Enmarcado en el campo de los Fundamentos Matemáticos de la Demostración Automática, realiza un estudio de las lógicas temporales proposionales, extensiones de la lógica clásica, definidas como álgebras abstractas, que permite la extensión a éstas de la metodología de demostración automática TAS. La metodología TAS se ha consolidado ya como una sólida alternativa a los trabajos existentes en demostración automática no clausal, como los métodos de Resolución y los métodos Tableaux. La herramienta fundamental de los métodos TAS es asociar a cada subfórmula de una fórmula en la lógica considerada una lista de implicantes e implicados; la información recogida en estas listas, se usará posteriormente para eldiseño de transformaciones de reducción. Por esta razón, en este trabajo desarrollamos una teoria de cierre completamente novedosa, sobre los Ideales/Filtros de literales Implicantes/Implicados de una fórmula, introduciendo las nociones de conjuntos a-cerrados y B-cerrados de literales y el concepto de base de estos conjuntos. Demostramos la unicidad de las bases y su propiedad de maximalidad sobre la cantidad de información por ellas recogida. Puesto que el objeto final es la aplicabilidad de nuestra investigación, en el desarrollo de este trabajo se estudian los aspectos computacionales de la teoría introducida, diseñando, en particular, algoritmos de gestión de los Ideales/Filtros de literales Implicantes/Implicados y del cálculo de las bases que, como se demuestra, tienen coste lineal.

Autor: GIL ESTALLO ANGEL JAVIER.
Año: 1995.
Universidad: BARCELONA.
Centro de lectura: MATEMATICAS.
Centro de realización: DEPARTAMENTO: LOGICA, HISTORIA Y FILOSOFIA DE LA CIENCIA PROGRAMA DE DOCTORADO: LOGICA MATEMATICA.

Resumen: SE DEFINE SISTEMA DE GENTZEN M-DIMENSIONAL COMO UNA PAREJA FORMADA POR UN LENGUAJE PROPOSICIONAL Y UNA RELACION DE CONSECUENCIA FINITARIA Y ESTRUCTURAL SOBRE EL CONJUNTO DE M-SECUENTES, SIENDO UN M- SECUENTE UNA EXPRESION DE LA FORMA (A1,...,AM) DONDE CADA AI ES UNA SUCESION FINITA DE FORMULAS. SE DEFINE FORMALMENTE EL CONCEPTO DE SISTEMA DE GENTZEN ACUMULATIVO Y DE TEOREMA DE LA DEDUCCION PARA UN SISTEMA DE GENTZEN. SE DEFINEN Y CARACTERIZAN LOS SISTEMAS DE GENTZEN M-DIMENSIONALES PROTOALGEBRAICOS Y SE ESTUDIA LA RELACION ENTRE ESTOS Y LA REGLA DE CORTE. SE DEFINE EL CONCEPTO DE EQUIVALENCIA ENTRE SISTEMAS DE GENTZEN Y SE DEFINEN LOS SISTEMAS DE GENTZEN ALGEBRIZABLES COMO AQUELLOS EQUIVALENTES AL SISTEMA DE GENTZEN NATURALMENTE ASOCIADO A UNA CIERTA CLASE DE ALGEBRAS. SE ESTUDIAN LAS PROPIEDADES GENERALES DE LOS SISTEMAS DE GENTZEN DETERMINADOS POR LOS CALCULOS DE M-SECUENTES VL (DEFINIDO POR M. BAAZ ET AL. "ELIMINATION OF CUTS IN FIRST-ORDER FINITE-VALUED LOGICS", 1994) Y RL (DEFINIDO POR G. ROUSSEAU "SEQUENTS IN MANY VALUED LOGIC I", 1967), DONDE L ES UNA ALGEBRA FINITA ARBITRARIA. FINALMENTE SE ESTUDIAN LOS SISTEMAS DE GENTZEN DETERMINADOS POR LOS CALCULOS DE SECUENTES VL EN CASO QUE L SEA UNA MV-ALGEBRA LINEAL Y FINITA DE M ELEMENTOS (EN RELACION CON LAS LOGICAS FINITAMENTE VALORADAS DE LUKASIEWICZ), O BIEN SEA UN RETICULO DISTRIBUTIVO PSEUDOCOMPLEMENTADO FINITO (EN RELACION CON LAS EXTENSIONES DEL FRAGMENTO SIN IMPLICACION DEL CALCULO PROPOSICIONAL INTUICIONISTA).

Autor: NIEVA SOTO SUSANA.
Año: 1990.
Universidad: COMPLUTENSE DE MADRID.
Centro de lectura: MATEMATICAS .
Centro de realización: DEPARTAMENTO: INFORMATICA Y AUTOMATICA PROGRAMA DE DOCTORADO: CIENCIAS DE LA COMPUTACION.

Resumen: EN LA PRIMERA PARTE DE LA MEMORIA SE PRESENTA UNA LOGICA COMPUTACIONAL, QUE ES UNA LOGICA DE PREDICADOS CON IGUALDAD EXTENDIDA CON POLIMORFISMO Y RECURSION, JUNTO CON UN SISTEMA DE DEDUCCION NATURAL, PARA ESTA LOGICA SE DA UNA DEFINICION PRECISA DE SU SEMANTICA Y SE DEMUESTRAN BUENAS PROPIEDADES. SE COMPRUEBA QUE ES ADECUADA PARA RAZONAR ACERCA DE FUNCIONES PARCIALES, MINIMO PUNTO FIJO DE FUNCIONALES Y SEMANTICA DENOTACIONAL, Y PARA HACER DEMOSTRACIONES MATEMATICAS. SE PRESENTA TAMBIEN UNA EXTENSION DE LOS TABLEAUX DE SHULLYAN DE PRIMER ORDEN QUE SUPONE EL USO DE ARBOLES W-RAMIFICADOS E INSTANCIAS MONOMORFICAS DE LAS FORMULAS DE PARTIDA. EL ALGORITMO DE LOS TABLEAUX SE UTILIZA COMO GUIA EN LA CONSTRUCCION DE CALCULOS COMPLETOS. UTILIZANDO ESTA PROPIEDAD SE CONSTRUYE UN SISTEMA DE REGLAS DE DEDUCCION NATURAL Y SE PRUEBA QUE COMO TODO CALCULO COMPLETO ES INFINITARIO. POR OTRO LADO, SE DEFINE EL CONCEPTO DE FORMULA CONTINUA Y SE INTRODUCE UN AXIOMA Y UNA REGLA DE INDUCCION BASADA EN EL MINIMO PUNTO FIJO. EN LA SEGUNDA PARTE DE LA MEMORIA, SE INTRODUCEN DIFERENTES TECNICAS PARA LA MECANIZACION DE DEMOSTRACIONES, BASADAS EN LOS CALCULOS DEFINIDOS EN LA PRIMERA PARTE Y SE ESTUDIA LA ESTRUCTURA EN FORMA DE ARBOL DE LAS DEMOSTRACIONES ANALIZANDO LA FORMA EN QUE TIENE LUGAR EL CONTROL. TAMBIEN SE FIJA LA SINTAXIS DEL LENGUAJE QUE SIRVE DE COMUNICACION USUARIO-SISTEMA MEDIANTE UNA GRAMATICA EN FORMA DE BACKUS-NAUR, DANDO UNA SERIE DE EJEMPLOS PRACTICOS. LA MEMORIA FINALIZA CON UNA BREVE DESCRIPCION DE LA IMPLEMENTACION DEL DEMOSTRADOR. EN EL ANEXO APARECEN LOS PROGRAMAS PROLOG.

Autor: MARTINEZ VIDAL M. CONCEPCION .
Año: 1988.
Universidad: VALENCIA.
Centro de lectura: FILOSOFIA Y CIENCIAS DE LA EDUCACION.
Centro de realización: FACULTAD DE FILOSOFIA Y CC. EDUCACION DE LA UNIVERSITAT DE VALENCIA.

Resumen: LA TESIS COMPRENDE DOS PARTES CLARAMENTE DIFERENCIADAS. EN UNA PRIMERA PARTE SE PRESENTA LA FILOSOFIA DE LA LOGICA DE PRAWITZ; EN CONCRETO SE DESCRIBEN LOS PRINCIPALES RESULTADOS OBTENIDOS POR ESTE AUTOR EN TEORIA GENERAL DE LA DEMOSTRACION Y SE ANALIZA EL PAPEL QUE DESEMPEÑAN LOS TEOREMAS DE NORMALIZACION EN EL CONCEPTO DE VALIDEZ INTENSIONAL QUE ESTE AUTOR PROPONE. EN LA SEGUNDA PARTE SE DESCRIBE UN SISTEMA LINEAL DE DEDUCCION NATURAL EN VERSION STANDAR Y VERSION DESTINADA A LA IMPLEMENTACION EN EL QUE LAS DERIVACIONES OBTENIDAS SON DERIVACIONES NORMALES. A PARTIR DE ESTE SISTEMA SE HA DISEÑADO UN MOTOR DE INFERENCIA CONSTRUCTIVO, DIRECTO, SINTACTICO, EURISTICO Y QUE PERMITE RECONSTRUIR LA DERIVACION GENERADA. EL OBJETIVO HA SIDO INICIAR LA INVESTIGACION QUE PERMITA DETERMINAR EN QUE MEDIDA LA MAS FACIL OBTENCION DE DEMOSTRACIONES QUE PERMITA EL SISTEMA COMPENSA LA ELIMINACION DE RODEOS ENTENDIDA COMO NO UTILIZACION DE LEMAS.