Optimización de la traducción funcional para lógicas modales

Abstract

En esta tesis estudiamos las traducciones funcionales que transforman fórmulas de lógica modal a lógica de primer orden con sorts. En trabajos previos se mostró que remover las anotaciones de sorts de las traducciones funcionales preserva satisfacibilidad. Investigamos el desempeño de SPASS, un demostrador de lógica de primer orden, al suministrarle fórmulas traducidas con y sin anotaciones de sorts. Concluimos que, para todas los casos testeados, remover sorts mejora el desempeño del demostrador.