Me pregunto si alguien me puede decir la diferencia entre Z3 y CoQ? Me parece que coq es un asistente de pruebas 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 una 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?Diferencia entre Z3 y coq
Coq es un demostrador de teoremas interactivo (también conocido como asistente de pruebas). Proporciona un lenguaje para escribir definiciones matemáticas, algoritmos y teoremas. También proporciona un entorno para producir pruebas controladas por 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 utilizaron Coq. Algunos afirman que, en el futuro, los sistemas como Coq serán ampliamente utilizados por los matemáticos. El article tiene un argumento convincente para pruebas formales en matemáticas. Recientemente, Georges Gonthier usó Coq para crear un comprobante comprobable del teorema de cuatro colores. Coq tiene un pequeño núcleo de confianza y proporciona una gran seguridad.
Z3 es un SMT (teorías de módulo de satisfaccion) solucionador. Su lenguaje es muchas teorías lógicas de primer orden clasificadas 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 usa principalmente en pruebas y verificación de software. También se puede usar para resolver restricciones, problemas de planificación, acertijos, 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 demostrador automático de teoremas. En Z3, las tácticas se usan para especificar domain specific strategies. Es decir, solucionadores personalizados para problemas en un dominio de aplicación particular. Z3 puede producir pruebas/certificados que se pueden verificar independientemente. Sin embargo, la generación de pruebas no es el enfoque principal del proyecto Z3. Además, muchos módulos no admiten la producción de pruebas y deben desactivarse cuando el usuario solicite 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 puede integrarse en aplicaciones más grandes. De hecho, ese es el caso para cada aplicación Z3 hasta ahora. Los usuarios finales no usan Z3 directamente. Está escondido dentro de herramientas como Isabelle, Pex, VCC, etc. El new Python front-end para Z3 intenta cambiar eso.