Reflection in general logics and in rewriting logic with applications to the maude languaje

Laburpena

La reflexión, entendida como la capacidad de representar nuestras ideas y de hacerlas objetos de nuestro propio pensamiento, ha sido reconocida desde hace muchos siglos como un rasgo clave de la inteligencia humana, En lógica, la reflexión ha sido estudiada con enorme interés por muchos investigadores desde los trabajos fundacionales de Godel y Tarski. En el ámbito de la informática ha sido un tema presente desde sus comienzos bajo la forma de las máquinas universales de Turing. El mismo éxito de las ideas reflexivas y la extensión de su aplicabilidad subraya la necesidad de dotar a los fenómenos reflexivos de fundamentos conceptuales. En este sentido, fundamentos metalógicos -para los que la lógica particular que se quiere elegir es un parámetro fácilmente cambiable- pueden ser muy útiles. En esta tesis proponemos nociones axiomáticas generales de lógicas reflexivas, lenguajes declarativos reflexivos y estrategias computaciones, que se basan en la teoría de lógicas generales. Un concepto clave en nuestro tratamiento axiomático de las lógicas reflexivas es la noción de una teoría universal, esto es, de una teoría U que puede simular las deducciones de todas las teorías dentro de una clase C de teorías de interés. En particular, si U es una de las teorías dentro de la clase C, entonces U puede simular su propio metanivel al nivel objeto, y este proceso puede ser iterado "ad infinitum" dando lugar a una "torre de reflexión". Además de proponer axiomas metalógicos generales, esta tesis estudia en profundidad la reflexión en una lógica particular, concretamente, la lógica de reescritura. Hemos demostrado en detalle que la lógica de reescritura satisface nuestra definición axiomática de lógica reflexiva. La reflexión es una propiedad de gran potencia y utilidad en la práctica. Por tanto, un aspecto clave en este trabajo ha sido explotar la reflexión en un amplio abanico de aplicaciones,