Métodos formales para normalización en lógica de primer orden usando la metodología tas

  1. Ojeda Aciego, Manuel
Dirixida por:
  1. Inmaculada Pérez de Guzmán Molina Director

Universidade de defensa: Universidad de Málaga

Ano de defensa: 1996

Tribunal:
  1. Francisco Andrés Triguero Ruiz Presidente/a
  2. Juan José Saameño Rodríguez Secretario/a
  3. José María Barja Pérez Vogal
  4. José Muñoz Pérez Vogal
  5. Sixto Romero Sánchez Vogal

Tipo: Tese

Teseo: 53809 DIALNET

Resumo

EN LA LOGICA DE PRIMER ORDEN LA OBTENCION DE FORMAS NORMALES ES UN PRERREQUISITO DE LOS METODOS DE DEMOSTRACION MAS EFICACES; PERO USUALMENTE LOS ALGORITMOS QUE REALIZAN ESA TAREA SON LA PARTE MAS DEBIL DE LOS MISMOS: EN ESTE TRABAJO SE PRESENTAN METODOS PARA OBTENER FORMAS PRENEXAS Y DE SKOLEM BASADOS EN LA METODOLOGIA TAS; CONSISTENTE EN UN FINO ANALISIS DEL ARBOL SINTACTICO DE LA FORMULA PARA DETECTAR TAUTOLOGIAS, CONTRADICCIONES O SUBFORMULAS EQUIVALENTES (O SIMULTANEAMENTE SATISFACIBLES) A OTRAS DE MENOR TAMAÑO; SU PRINCIPAL OBJETIVO ES RETRASAR TODO LO POSIBLE LA TAREA QUE PRODUCE LA COMPLEJIDAD EXPONENCIAL: LA DISTRIBUCION, Y EN TODO CASO REALIZARLA DE MODO EFICIENTE Y PARALELO,UN SUTIL ANALISIS SOBRE LA DEPENDENCIA DE VARIABLES Y EL APROVECHAMIENTO DE LAS POSIBILIDADES DE SIMPLIFICACION DE LA FORMA NORMAL NEGATIVA PERMITE PROPORCIONAR FORMAS NORMALES SORPRENDENTEMENTE SIMPLES EN MUCHOS CASOS, LO CUAL HACE DE LOS METODOS INTRODUCIDOS UNAS HERRAMIENTAS EXTRAORDINARIAMENTE UTILES EN EL CAMPO DE LA DEMOSTRACION AUTOMATICA.