Automated deduction with constrained clauses

• Autores: Albert Rubio Gimeno
• Directores de la Tesis: Robert Nieuwenhuis (dir. tes.)
• Lectura: En la Universitat Politècnica de Catalunya (UPC) ( España ) en 1994
• Idioma: inglés
• Tribunal Calificador de la Tesis: Fernando Orejas Valdés (presid.) , Josep Díaz Cort (secret.) , María Alpuente Frasnedo (voc.) , Leo Bachimair (voc.) , Pierre Jonannaud Jean (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • ESTA TESIS DOCTORAL SE CENTRA EN EL ESTUDIO DE MECANISMOS PARA REALIZAR DEDUCCION AUTOMATICA EN LOGICA DE PRIMER ORDEN CON IGUALDAD, LA DEMOSTRACION AUTOMATICA DE TEOREMAS SE ESTA APLICANDO ACTUALMENTE EN MUCHAS AREAS DE LA INFORMATICA COMO SON LA INGENIERIA DE SOFTWARE, LAS BASES DE DATOS O LA INTELIGENCIA ARTIFICIAL.

    LOS RESULTADOS DE LA TESIS SE PUEDEN DIVIDIR EN: LOS CONSIDERADOS BASICOS, COMO SON EN LA DEFINICION DE ORDENES SOBRE TERMINOS (O EXPRESIONES) EN LA RESOLUCION DE RESTRICCIONES SIMBOLICAS, CUYA UTILIDAD VA MAS ALLA DE SU APLICACION EN ESTE TRABAJO; Y LES RESULTADOS EN DEDUCCION AUTOMATICA, QUE INCLUYE RESULTADOS DE COMPLETITUD REFUTACIONAL PARA PROCESOS DE DEDUCCION MEDIANTE CLAUSULAS CON RESTRICCIONES DE IGUALDAD (TAMBIEN LLAMADAS ESTRATEGIAS BASICAS) Y DE ORDEN, CONSIDERANDO ADEMAS EL PREDICADO DE IGUALDAD COMO PREDEFINIDO Y DANDO LA POSIBILIDAD DE TRABAJAR MODULO ALGUNA TEORIA EQUACIONAL.