Usando el ambiente Maude para la demostración semi-automática de teoremas en lógica temporal lineal de primer orden
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....
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Español |
| Publicado: |
2005
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/23074 |
| Aporte de: |
| Sumario: | 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 |
|---|