Adrianistán

El blog de Adrián Arroyo


Artículos con etiqueta «z3»

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.

Seguir leyendo