Diferencia entre Z3 y coq.

theorem-proving

Question

Me pregunto si alguien puede decirme la diferencia entre Z3 y coq. Me parece que coq es un asistente de prueba, ya que requiere que el usuario complete los pasos de prueba, mientras que Z3 no tiene ese requisito. Pero parece que coq también tiene táctica automática que es similar a lo que hace Z3? ¿O tal vez la capacidad de búsqueda de pruebas en coq no es tan poderosa como Z3?

Answer 1

Coq es un proverbio de teoremas interactivo (también conocido como asistente de prueba). Proporciona un lenguaje para escribir definiciones matemáticas, algoritmos y teoremas. También proporciona un entorno para la producción de pruebas comprobadas a máquina. Coq se ha utilizado para formalizar teoremas matemáticos y proporcionar la semántica de los lenguajes de programación. Hoy en día, podemos encontrar muchos artículos en POPL que usaron Coq. Algunos afirman que, en el futuro, los matemáticos utilizarán ampliamente sistemas como Coq. El article tiene un argumento convincente para las pruebas formales en matemáticas. Recientemente, Georges Gonthier usó Coq para crear una prueba encuestable del teorema de los cuatro colores. Coq tiene un núcleo de confianza pequeño y proporciona alta seguridad.

Z3 es un solucionador de SMT (teorías de modulo de satisfacción). Su lenguaje consta de muchas teorías lógicas + ordenadas de primer orden, como aritmética, vectores de bits, tipos de datos, matrices, etc. Este lenguaje no es tan expresivo como el utilizado en Coq. Z3 tampoco tiene soporte para la gestión de pruebas como Coq. Z3 se utiliza principalmente en pruebas y verificación de software. También se puede utilizar para resolver restricciones, problemas de planificación, rompecabezas, etc. Hay un gran énfasis en encontrar modelos (es decir, soluciones) para fórmulas satisfactorias. El article describe muchas aplicaciones Z3 dentro de Microsoft y en otros lugares. Z3 es esencialmente un proverbio de teoremas automático. En Z3, las tácticas se utilizan para especificar estrategias específicas de dominio . Es decir, solucionadores personalizados para problemas en un dominio de aplicación particular. Z3 puede producir pruebas / certificados que pueden verificarse independientemente. Sin embargo, la generación de pruebas no es el foco principal del proyecto Z3. Además, muchos módulos no admiten la producción de pruebas y se deben desactivar cuando el usuario solicita la generación de pruebas. Z3 también se ha integrado en asistentes de prueba como Isabelle , y algunos están trabajando en la integración de Z3 en Coq. La idea es tener lo mejor de ambos mundos: lenguaje muy expresivo y muy buena automatización. Z3 también se puede ver como un motor de razonamiento lógico que se puede incrustar en aplicaciones más grandes. De hecho, ese es el caso de todas las aplicaciones Z3 hasta ahora. Los usuarios finales no usan Z3 directamente. Está oculto dentro de herramientas como Isabelle, Pex , VCC , etc. El nuevo front-end de Python para Z3 intenta cambiar eso.