Reflection in general logics and in rewriting logic with applications to the maude languaje
Manuel Clavel · 1998
La reflexion, 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 logica, la reflexion ha sido estudiada con enorme interes por muchos investigadores desde los trabajos fundacionales de Godel y Tarski. En el ambito de la informatica ha sido un tema presente desde sus comienzos bajo la forma de las maquinas universales de Turing. El mismo exito de las ideas reflexivas y la extension de su aplicabilidad subraya la necesidad de dotar a los fenomenos reflexivos de fundamentos conceptuales. En este sentido, fundamentos metalogicos -para los que la logica particular que se quiere elegir es un parametro facilmente cambiable- pueden ser muy utiles. En esta tesis proponemos nociones axiomaticas generales de logicas reflexivas, lenguajes declarativos reflexivos y estrategias computaciones, que se basan en la teoria de logicas generales. Un concepto clave en nuestro tratamiento axiomatico de las logicas reflexivas es la nocion de una teoria universal, esto es, de una teoria U que puede simular las deducciones de todas las teorias dentro de una clase C de teorias de interes. En particular, si U es una de las teorias 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 reflexion. Ademas de proponer axiomas metalogicos generales, esta tesis estudia en profundidad la reflexion en una logica particular, concretamente, la logica de reescritura. Hemos demostrado en detalle que la logica de reescritura satisface nuestra definicion axiomatica de logica reflexiva. La reflexion es una propiedad de gran potencia y utilidad en la practica. Por tanto, un aspecto clave en este trabajo ha sido explotar la reflexion en un amplio abanico de aplicaciones,