¿Es posible traducir una fórmula booleana B en una conjunción equivalente de cláusulas Horn? El artículo de Wikipedia sobre HornSAT parece implicar que lo es, pero no he podido perseguir ninguna referencia. Tenga en cuenta que no me refiero a "en tiempo polinómico", sino más bien "en...
Parece que George Gonthier y sus colaboradores han terminado de formalizar el Teorema de la orden impar . En su trabajo anterior sobre el Teorema de los cuatro colores, Gonthier inventó un montón de nuevos algoritmos (en su mayoría variantes de BDD y algoritmos de gráficos) que eran especialmente...
Esta pregunta se migró de Stack Overflow porque se puede responder en el intercambio teórico de Stack Computer Science. Migrado hace 8 años . Dado que la correspondencia de Curry-Howard está tan extendida / extendida, ¿hay alguna diferencia entre pruebas y programas (o...
Considere esta pregunta resuelta. No elegiré la mejor respuesta ya que todas ellas han contribuido a mi comprensión del tema. No estoy seguro de qué beneficio tenemos al definir formalmente la semántica de la lógica de predicados. Pero sí valoro tener un cálculo de prueba formal. Mi punto es que...
He estado leyendo mucho sobre sistemas de tipos y tal, y entiendo aproximadamente por qué se introdujeron (para resolver la paradoja de Russel). También entiendo aproximadamente su relevancia práctica en lenguajes de programación y sistemas de prueba. Sin embargo, no estoy completamente seguro de...
ACSL (Ansi C Specification Language), es una especificación para el código C, anotada con comentarios especiales, que permite verificar formalmente el código C. No lo he investigado , pero imagino que los métodos formales utilizados en los verificadores ACSL serían similares a Hoare Logic. Sin...
Quiero hacer un primer solucionador SAT. Conozco la competencia SAT y la conferencia SAT, y hay tantos documentos sobre este tema. Soy un abridor, un abrumador abrumador. ¿Dónde debería comenzar? Finalmente quiero impulsar el estado del arte. Quiero un consejo experto sobre cómo comenzar, para no...
Tipos y lenguajes de programación se enfoca bastante en el subtipo, pero por lo que puedo decir, el subtipo no parece especialmente fundamental. ¿El subtipo le da algo más que los tipos dependientes? Trabajar con tipos dependientes seguramente será más trabajo, por lo que puedo entender por qué los...
En su respuesta a esta pregunta , Stephane Giménez me señaló un algoritmo de normalización de tiempo polinómico para pruebas en lógica lineal. La prueba en el documento de Girard utiliza redes de prueba, que son un aspecto de la lógica lineal que realmente no conozco mucho. Ahora, he tratado de...
Recientemente he visto varios artículos sobre arxiv que se refieren a un sistema de prueba llamado suma de cuadrados. ¿Alguien puede explicar qué es una prueba de suma de cuadrados y por qué esas pruebas son importantes / interesantes? ¿Cómo se relacionan con otros sistemas de prueba algebraica?...
Por lo que entiendo (que es muy poco, ¡así que corrígeme donde me equivoco!), La teoría de los lenguajes de programación a menudo se ocupa de las pruebas "intuicionistas". En mi propia interpretación, el enfoque requiere que tomemos en serio las consecuencias del cálculo en la lógica y la...
¿Alguien sabe de referencias que explican con precisión la conexión entre el algoritmo de unificación y la eliminación gaussiana? Estoy particularmente interesado en la relación entre las sustituciones triangulares y las descomposiciones LU. Wayne Snyder y Jean Gallier mencionan esta analogía de...
Actualmente doy un pequeño curso (cuatro conferencias de dos horas a nivel de maestría) sobre Métodos lógicos en seguridad , aunque el título Métodos formales en seguridad podría ser más adecuado. Cubre brevemente los siguientes temas (con métodos lógicos asociados): Gestión de derechos digitales...
He leído que inicialmente Church propuso el cálculo como parte de su artículo Postulados de lógica (que es una lectura densa). Pero Kleene demostró que su "sistema" era inconsistente, después de lo cual Church extrajo cosas relevantes para su trabajo sobre "computabilidad efectiva" y abandonó su...
¿Alguien podría explicar la diferencia entre: Tipos de datos algebraicos (con los que estoy bastante familiarizado) Tipos de datos algebraicos generalizados (¿qué los hace generalizados?) Tipos inductivos (por ejemplo, Coq) (Especialmente tipos inductivos.)
He visto (y he oído) que afirmaba que es seguro agregar el axioma clásico del medio excluido a Coq, pero parece que no puedo encontrar un documento que respalde esta afirmación. Los documentos que veo enumerados en el wiki de Coq sobre el medio excluido muestran inconsistencia con el conjunto...
Considere el siguiente razonamiento: Deje que denote la complejidad de Kolmogorov de la cadena x . El teorema de incompletitud de Chaitin dice queK( x )K(x)K(x)Xxx para cualquier sistema coherente y suficientemente fuerte formales , existe una constante T (dependiendo sólo del sistema formal y...
Un objetivo importante de los métodos formales es demostrar la corrección de los sistemas, ya sea por medios automatizados o dirigidos por humanos. Sin embargo, parece que incluso si puede proporcionar una prueba de corrección, es posible que NO pueda garantizar que el sistema no falle. Por...
La autorreferencialidad del problema P / NP a veces se ha resaltado como una barrera para su resolución, ver, por ejemplo, el artículo de Scott Aaronson, ¿ es P vs. NP formalmente independiente ? Una de las muchas resoluciones concebibles para P / NP sería una demostración de que el problema es...
Es bien sabido que los combinadores S y K son Turing completos. ¿Hay combinadores que sean suficientes para producir (solo) las funciones recursivas