Metateoremas sobre grafos : el Teorema de Courcelle (2020)
En el presente documento se estudia la demostración del meta-teorema de Courcelle. Este último es un resultado sobre grafos y lógica que enuncia que, para cualquier entero k, cualquier propiedad de grafos que sea expresable en lógica monádica de segundo orden (en el lenguaje de grafos), es decidible en tiempo lineal, si uno se restringe a la clase de k- árboles parciales (es decir, aquellos con anchura de árbol a lo sumo k). En términos generales, la demostración de este teorema de complejidad parametrizada se apoya en la existencia de dos algoritmos de complejidad lineal: 1.Algoritmo 1: Dada una sentencia S que representa una propiedad de grafos, construye un autómata de árbol que verifica la sentencia. Nota: Un autómata de árbol es un autómata de estados finitos que se ejecuta, no sobre cadenas (como será en un D.F.A clásico), sino sobre árboles con nodos marcados con caracteres de un alfabeto. 2. Algoritmo 2: Dado un grafo, construye una descomposición de árbol de anchura a lo sumo k para el grafo (si existe), normalizada, que sirve para construir un parse tree. Una parte importante del algoritmo 2 utiliza el algoritmo de Bodlaender, el cual enunciamos sin demostración de su corrección. Una vez hechas estas construcciones, se concluye el teorema principal como consecuencia de ejecutar el autómata con el parse tree construido como entrada