Portal de Periódicos da CAPES

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

2007; Asociación Española para la Inteligencia Artificial; Volume: 8; Issue: 23 Linguagem: Espanhol

10.4114/ia.v8i23.790

1988-3064

Manuel Enciso, I. P. del Guzman, C. Rossi,

Formal Methods in Verification

Una forma normal temporal independiente del metodo de deduccion. En este trabajo se presenta la definicion de una forma normal para una logica modal temporal. Como logica objetivo hemos elegido la logica LNint-e, que destaca por tratarse de una logica que combina puntos e intervalos y disponer simultaneamente 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 metodo de deduccion. De este modo, dicha forma normal puede ser usada por cualquierdemostrador automatico de teoremas, con diferentes paradigmas (resolucion, tablas semanticas, etc.) e incluso ser incorporada a metodos de deduccion como el chequeo de modelos para aumentar el rendimiento de estos. Asi, en el proceso de normalizacion se busca esencialmente reducir la complejidad de las expresiones logicas en lugarde preparar esta para un determinado tratamiento automatico. La definicion introducida se basa principalmente en el concepto de literal temporal. Este concepto permite la construccion de transformaciones de equivalencia que reducen la complejidad de la formula de entrada. Entre estas transformaciones conviene destacar por su novedad aquellas que permiten la eliminacion de conectivas temporales binarias,que suponen un mayor coste de procesamiento en los metodos de pruebas. Los beneficios de este trabajo han sido comprobados empiricamente mediante una implementacion del metodo, cuyos resultados se comentan tambien eneste trabajo.