RT Generic T1 Demostración de reducibilidad entre problemas utilizando Dafny T1 Proving problems reducibility using Dafny A1 Starry González, David Alfonso AB En este trabajo se pretende demostrar la reducibilidad polinómica entre problemas NP-completos utilizando un lenguaje formal. En particular se utiliza el lenguaje Dafny, que permite especificar y verificar programas que contienen instrucciones tanto imperativas como funcionales. Primero se hará una introducción al lenguaje de programación Dafny, la NPcompletitud, los problemas que se verán a lo largo del trabajo y la reducibilidad polinómica.A continuación se formalizan las definiciones de los problemas y se implementan métodos de verificación polinómicos que demuestran la pertenencia de los problemas al conjunto NP. Finalmente se definen las transformaciones polinómicas entre dichos problemas que permiten demostrar la reducibilidad polinómica entre ellos. AB The aim of this paper is to prove polynomial reducibility between NP-complete problems using a formal language. In particular, the Dafny language is used, which allows to specify and verify programs containing both imperative and functional instructions. First, an introduction to the Dafny programming language, NP-completeness, the problems that will be seen throughout the paper, and polynomial reducibility will be given. Then the definitions of the problems are formalized and polynomial verification methods that prove the membership of the problems to the NP-set are implemented. Finally, we define the polynomial transformations between these problems that allow us to prove polynomial reducibility between them. YR 2025 FD 2025 LK https://hdl.handle.net/20.500.14352/123859 UL https://hdl.handle.net/20.500.14352/123859 LA spa NO Trabajo de Fin de Grado en Grado en Ingeniería Informática, Facultad de Informática UCM, Departamento de Sistemas Informáticos y Computación, Curso 2024/2025. En este Github se encuentra todo el código y otros materiales complementarios del TFG: https://github.com/DavidSG/TFG/tree/main DS Docta Complutense RD 12 sept 2025