Resumen de lecturas compartidas durante enero de 2020

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas, durante enero de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante enero de 2020”

Reseña: A formalised polynomial-time reduction from 3SAT to Clique

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre SAT titulado A formalised polynomial-time reduction from 3SAT to Clique.

Sus autor es Lennard Gäher del Programming Systems Lab en la Universidad del Sarre (en inglés, Saarland University y en alemán Universität des Saarlandes) en Saarbrücken, Alemania.

Su resumen es

We present a formalisation of the well-known problems SAT and Clique from computational complexity theory. From there, a polynomial-time reduction from 3SAT, a variant of SAT where every clause has exactyly three literals, is developed and verified. All the results are constructively formalised in the proof assistant Coq, including the polynomial running time bounds. The machine model we use is the weak call-by-value lambda calculus.

El trabajo forma parte de su Bachelor’s Thesis y está dirigido por Fabian Kunze.

Resumen de lecturas compartidas del 25 al 31 de enero de 2020

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas, del 25 al 31 de enero, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.

Read More “Resumen de lecturas compartidas del 25 al 31 de enero de 2020”