Título: Usando el ambiente Maude para la demostración semi-automática de teoremas en lógica temporal lineal de primer orden
Autores: Mac Donnell, Patricio
Aguirre, Nazareno Matías
Fecha: 2012-10-26
2005-10
2005-10
Publicador: Unversidad Nacional de La Plata
Fuente:

Tipo: Objeto de conferencia
Objeto de conferencia
Tema: Temporal logic
Programming Environments
Ciencias Informáticas
Descripción: 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
II Workshop de Ingeniería de Software y Bases de Datos (WISBD)
Idioma: Español