Artículos con etiqueta «z3»
Teletexto #012
Ya iba siendo hora de otro teletexto, ¿no creéis? Pues sí, ha pasado ya un tiempo y mi lista de enlace ha crecido enormemente. Vamos con algunos de ellos.
Introducción a Z3, el demostrador de teoremas de Microsoft
Z3 es un demostrador de teoremas open source creado por Microsoft. Una herramienta muy útil para resolver ciertos problemas de alta complejidad algortítmica. Z3 en particular se enfoca en la resolución SMT. En este artículo veremos como podemos usarlo para resolver problemas sencillos y no tan sencillos. Se trata de otro lenguaje dentro del mundo de la programación lógica, como Prolog, pero bastante más específico.