Resumen de Lógica temporal y demostración automática de teoremas. Eficiencia y paralelismo
ESTE TRABAJO SE ENMARCA EN LA DEMOSTRACION AUTOMATICA DE TEOREMAS EN LOGICA MODAL Y, MAS CONCRETAMENTE EN LA LOGICA MODAL TEMPORAL, SU OBJETIVO ES HACER DE LA LOGICA MODAL TEMPORAL UNA HERRAMIENTA UTIL Y ATRACTIVA PARA LAS CIENCIAS DE LA COMPUTACION, CONSIGUIENDO UN TRATAMIENTO SEMANTICO ADECUADO Y DEMOSTRADORES AUTOMATICOS QUE MEJOREN LA EFICIENCIA DE LOS YA EXISTENTES.
EN ESTE TRABAJO SE INTRODUCEN LOS METODOS TAS-KT+ Y TAS-FNEXT QUE SON DEMOSTRADORES AUTOMATICOS DE TEOREMAS PARA EL FRAGMENTO DE FUTURO DE LA LOGICA MINIMAL KT Y DE LA LOGICA TEMPORAL LINEAL PARA TIEMPO DISCRETO E INFINITO RESPECTIVAMENTE.
AMBOS METODOS SON METODOS POR REFUTACION Y DE CONSTRUCCION DE MODELOS Y TIENEN LAS SIGUIENTES CARACTERISTICAS:
- ESTAN FUERTEMENTE BASADOS EN LA ESTRUCTURA DEL ARBOL SINTACTICO DE LA FORMULA.
- FUNCIONAN POR APLICACION PROGRESIVA DE UNA SERIE DE TRANSFORMACIONES. DICHAS TRANSFORMACIONES SON TODAS DE COMPLEJIDAD A LO SUMO POLINOMICA SALVO LA ULTIMA DE ELLAS, QUE SOPORTA EL PESO EXPONENCIAL DEL PROBLEMA.
- LAS TRANSFORMACIONES SON DE DOS TIPOS:
TRANSFORMACIONES DE EQUIVALENCIA Y TRANSFORMACIONES QUE CONSERVAN LA SATISFACIBILIDAD. EL OBJETIVO DE ESTAS TRANSFORMACIONES ES CONSEGUIR REDUCIR EL TAMAÑO DE LA FORMULA ANTES DE APLICAR LA ULTIMA DE ELLAS (INCLUSO EVITANDO SU APLICACION SI ES POSIBLE).
ESTE OBJETIVO SE CONSIGUE COMBINANDO INFORMACION SINTACTICA Y SEMANTICA QUE PERMITE DETECTAR SUBFORMULAS VALIDAS, INSATISFACIBLES O EQUIVALENTES A OTRAS MAS SENCILLAS.
LOS METODOS TRABAJAN SOBRE FORMULAS DE LA LOGICA MODAL TEMPORAL SIN NINGUN TRATAMIENTO SINTACTICO PREVIO; ES DECIR, SIN PRODUCIR UNA NORMALIZACION DE LAS EXPRESIONES COMO EN LOS METODOS BASADOS EN RESOLUCION.
