Formalización de aspectos de la Irredundancia Superior de Máximo Peso

MAURICIO SALICHS; DANIEL SEVERÍN; RICARDO D. KATZ

Congreso; LXIX Reunión anual de Comunicaciones Científicas de la Unión Matemática Argentina (virtUMA 2020); 2020

Dado un grafo G = (V, E) y un vector de pesos w, denotamos con IR_w(G) al peso máximo de un conjunto irredundante, donde un conjunto irredundante D se define como aquel para el que cada vértice v en D tiene al menos un vértice privado. El Problema de Irredundancia Superior de Máximo Peso (PISMP) consiste justamente en hallar dicho parámetro. D. Severín y G. Nasini establecieron una reducción polinomial del PISMP al Problema del Conjunto Estable de Máximo Peso (PCEMP), lo que permitió probar que el PISMP es polinomial sobre ciertas familias de grafos. Sin embargo esta prueba requiere de la separación y comprobación de gran cantidad de casos, por lo que se optó por la verificación formal con un asistente de prueba (ya hay antecedentes de este tipo de técnica, como es el caso de la formalización del Teorema de los Cuatro Colores en el lenguaje Coq). En este trabajo, realizado en el marco de la tesina de M. Salichs, se formalizó la reducción polinomial del PISMP al PCEMP y la prueba de que si G contiene a P_4 o K_{2,3} inducido entonces G´ contiene a P_4 inducido, y si G contiene a claw, bull, P_6 o el complemento de C_6 entonces G´ contiene a claw, donde G´ es el grafo de la instancia del PCEMP resultante de la reducción mencionada. La formalización se realiza en el lenguaje Coq con la extensión Ssreflect y la librería MathComp que proveen una plataforma para la realización de pruebas constructivas. Además se utilizan las muy recientes librerías de teoría de grafos y de dominación desarrolladas por C. Doczkal, D. Pous y D. Severín. La Formalización de la Matemática es una rama reciente de las Ciencias de la Computación que aun no se ha desarrollado lo suficiente como para que los matemáticos la adopten, pero que permite garantizar la correctitud de grandes teoremas, como el de los Cuatro Colores. Recientemente se han formalizado varios resultados de la teoría de grafos, como: Teorema de Menger, caracterización por menores de grafos con treewidth 2, cadena de Cockayne-Hedetniemi, Lema de Replicación de Lovász y Teorema Débil de Grafos Perfectos.