Me gustaría escribir pruebas matemáticas con algún asistente de prueba. Todo se escribirá utilizando la lógica de primer orden (con igualdad) y la deducción natural. El fondo es la teoría de conjuntos (ZF). Por ejemplo, ¿cómo podría escribir la siguiente prueba?
Axioma:
Teorema:
Es decir, el conjunto vacío es único.
Es trivial para mí lograr eso usando papel y un bolígrafo, pero lo que realmente necesito es un software que me ayude a verificar la corrección de la prueba.
Gracias.
Respuestas:
Tanto Coq como Isabelle pueden hacer esto.
[Coq] Aquí hay un artículo que discute cómo codificar ZFC en CIC, en el que se basa Coq.
Benjamin Werner: Conjuntos en tipos, Tipos en conjuntos (1997). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709
[Isabelle] Hay una biblioteca para ZF.
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html
fuente
Movido del comentario por sugerencia de Kaveh
Primero debe seleccionar un asistente de prueba. Coq es lo que uso, pero hay muchos otros . Coq se basa en la lógica de orden superior (el llamado cálculo de construcciones inductivas). Otros asistentes de prueba se basan en la lógica de primer orden, por lo que pueden ser más adecuados para sus necesidades (modulo de los comentarios anteriores).
Entonces debes comprometerte a aprender el asistente de pruebas. El documento vinculado es un tutorial para despegar con Coq. Convertirse en un experto en Coq requiere años de dedicación y práctica, pero los teoremas simples se pueden probar en una tarde. La clave para aprender Coq o cualquier otro asistente de pruebas es hacer pruebas, como las que se encuentran en el documento vinculado. Solo leer el documento ayudará muy poco, porque toda la experiencia de interactuar con el asistente de pruebas no se puede transmitir bien en papel.
En unos pocos días, debería poder codificar teoremas simples, como el anterior, y probarlos. No esperes que haremos esto por ti. No aprenderás nada de esa manera.
Cuando logre probar estos teoremas, no dude en publicar sus respuestas aquí y tal vez dejar algunos comentarios sobre sus experiencias.
¿Estás preparado para el reto?
fuente
Hay muchos artículos de matemáticas escritos con el asistente de pruebas Mizar: http://mizar.org/fm/
fuente
Dave Clarke sugiere Coq, pero en realidad Isabelle parece una idea mucho mejor, ya que tiene una biblioteca A para ZF . Isabelle también es muy madura e incluye una amplia variedad de tácticas y extensiones.
Personalmente no he usado Mizar, pero también puede ser bueno.
fuente
En Isabelle / ZF puedes escribir algo como esto
Como puede ver, Isabelle lo prueba automáticamente. Por supuesto, puede escribir una prueba más detallada si realmente lo desea.
fuente
Este mismo teorema es un ejemplo trabajado (ver Ejemplo 11) en el tutorial incluido con mi software DC Proof 2.0. Descárguelo gratuitamente en mi sitio web http://www.dcproof.com
fuente