Usando el ambiente Maude para la demostración semi-automática de teoremas en lógica temporal lineal de primer orden

Abstract

En este artículo, presentamos una implementación modular de un demostrador semi-automático de teoremas para la lógica temporal lineal de primer orden, realizada en el ambiente Maude. Maude es un ambiente de programación y especificación, basado en la lógica de reescritura, propuesta por J. Meseguer. Entre las aplicaciones de la lógica de reescritura, se destaca la aplicación de ´esta como ambiente para la implementación de otras lógicas. Aprovechamos en este artículo esta singular característica de la lógica de reescritura, y la simplicidad, expresividad y eficiencia de Maude, para construir un demostrador de teoremas interactivo, para la lógica temporal lineal de primer orden, basado en un cálculo de secuentes para ésta