Reflexión, abstracción y simulación en la lógica de reescritura

Resumen

La lógica de reescritura es una extensión de la lógica ecuacional habitual que fue introducida como un modelo parala especificación de sistemas concurrentes que unifica numerosas propuestas anteriores, Desde entonces esta lógica ha demostrado ser un formalismo muy flexible, no solo para la especificación de la concurrencia, sino también como marco lógico y semántico en el que interpretar otras lógicas y modelos de computación. Desde su introducción, se presentó tal lógica como la base de un lenguaje declarativo de especificación y programación, llamado Maude. El estudio de las propiedades matemáticas de la lógica de reescritura es necesario para justificar su uso como herramienta de diseño y especificación. Una de estas propiedades, de fundamental importancia en esta lógica, es la reflexión, que intuitivamente consiste en la habilidad de un sistema computacional o lógico de acceder a su propio metanivel para controlar su comportamiento. En esta tesis damos una demostración detallada de la reflexividad de la lógica de reescritura que extiende trabajos previos sobre versiones más restringidas de la lógica. Además, presentamos un enfoque unificador, aprovechando el trabajo anterior para el estudio de la reflexión en algunas sublógicas de la lógica de reescritura como son la lógica de pertenencia a la lógica de horn con igualdad. La reflexión en la lógica de reescritura tiene, además, una vertiente claramente práctica en la que se propone el uso de la reflexión para metarrozanamiento formal. En esta tesis se avanza en estas ideas, generalizando los principios inductivos propuestos por otro autores y estudiando cómo aplicarlos para demostrar relaciones semánticas entre teorías en la lógica de pertenencia. El otro gran tema de la tesis consiste en la búsqueda de métodos de demostración para la verificación de sistemas que con ella se especifiquen. Para la verificación de propiedades en sistema