Resumen de Una forma normal temporal independiente del método de deducción

Carlos Rossi , Manuel Enciso García-Oliveros , Inmaculada Pérez de Guzmán Molina

• Una forma normal temporal independiente del metodo de deducción. En este trabajo se presenta la definición de una forma normal para una lógica modal temporal. Como lógica objetivo hemos elegido la lógica LNint-e, que destaca por tratarse de una lógica que combina puntos e intervalos y disponer simultáneamente de un tratamiento del tiempo absoluto y relativo. Nuestro principal objetivo al definir la forma normal ha sido dotarla de una absoluta independencia respecto al método de deducción. De este modo, dicha forma normal puede ser usada por cualquierdemostrador automático de teoremas, con diferentes paradigmas (resolución, tablas semánticas, etc.) e incluso ser incorporada a métodos de deducción como el chequeo de modelos para aumentar el rendimiento de estos. Así, en el proceso de normalización se busca esencialmente reducir la complejidad de las expresiones lógicas en lugarde preparar esta para un determinado tratamiento automático. La definición introducida se basa principalmente en el concepto de literal temporal. Este concepto permite la construcción de transformaciones de equivalencia que reducen la complejidad de la fórmula de entrada. Entre estas transformaciones conviene destacar por su novedad aquellas que permiten la eliminación de conectivas temporales binarias,que suponen un mayor coste de procesamiento en los métodos de pruebas. Los beneficios de este trabajo han sido comprobados empíricamente mediante una implementación del método, cuyos resultados se comentan también eneste trabajo.