El sistema Mizar consta de un lenguaje formal para la redacción de definiciones y pruebas matemáticas, un asistente de pruebas , que es capaz de verificar mecánicamente las pruebas escritas en este lenguaje, y una biblioteca de matemáticas formalizadas , que se puede utilizar en la demostración de nuevos teoremas. [1] El sistema es mantenido y desarrollado por el Proyecto Mizar, anteriormente bajo la dirección de su fundador Andrzej Trybulec .
Captura de pantalla | |
Paradigma | Declarativo |
---|---|
Diseñada por | Andrzej Trybulec |
Apareció por primera vez | 1973 |
Disciplina de mecanografía | Débil , estático |
Extensiones de nombre de archivo | .miz .voc |
Sitio web | www.mizar.org |
Influenciado por | |
Automath | |
Influenciado | |
Modos OMDoc , HOL Light y Coq mizar |
En 2009, la Biblioteca de Matemáticas Mizar era el mayor cuerpo coherente de matemáticas estrictamente formalizadas que existía. [2]
Historia
El Proyecto Mizar fue iniciado alrededor de 1973 por Andrzej Trybulec como un intento de reconstruir la lengua vernácula matemática para que pueda ser verificado por una computadora. [3] Su objetivo actual, además del desarrollo continuo del Sistema Mizar, es la creación colaborativa de una gran biblioteca de pruebas verificadas formalmente, que cubra la mayor parte del núcleo de las matemáticas modernas. Esto está en línea con el influyente manifiesto QED . [4]
Actualmente, el proyecto es desarrollado y mantenido por grupos de investigación de la Universidad de Białystok , Polonia, la Universidad de Alberta , Canadá y la Universidad de Shinshu , Japón. Si bien el corrector de pruebas de Mizar sigue siendo propietario, [5] la Biblioteca Matemática de Mizar, el considerable cuerpo de matemáticas formalizadas que verificó, tiene licencia de código abierto. [6]
Los artículos relacionados con el sistema Mizar aparecen regularmente en las revistas revisadas por pares de la comunidad académica de formalización matemática. Estos incluyen estudios en lógica, gramática y retórica , matemáticas informáticas inteligentes , demostración interactiva de teoremas , Revista de razonamiento automatizado y Revista de razonamiento formalizado .
Lengua mizar
El rasgo distintivo del lenguaje Mizar es su legibilidad. Como es común en el texto matemático, se basa en la lógica clásica y un estilo declarativo . [7] Los artículos de Mizar están escritos en ASCII ordinario , pero el lenguaje fue diseñado para estar lo suficientemente cerca de la lengua vernácula matemática para que la mayoría de los matemáticos pudieran leer y comprender los artículos de Mizar sin una formación especial. [1] Sin embargo, el lenguaje permite el mayor nivel de formalidad necesario para la verificación de pruebas automatizada .
Para que una prueba sea admitida, todos los pasos deben justificarse mediante argumentos lógicos elementales o citando pruebas verificadas previamente. [8] Esto da como resultado un mayor nivel de rigor y detalle que el habitual en los libros de texto y publicaciones de matemáticas. Por lo tanto, un artículo típico de Mizar es aproximadamente cuatro veces más largo que un documento equivalente escrito en estilo ordinario. [9]
La formalización es relativamente laboriosa, pero no increíblemente difícil. Una vez que uno está familiarizado con el sistema, se necesita aproximadamente una semana de trabajo a tiempo completo para verificar formalmente la página de un libro de texto. Esto sugiere que sus beneficios están ahora al alcance de campos aplicados como la teoría de la probabilidad y la economía . [2]
Biblioteca Matemática Mizar
La Biblioteca Matemática de Mizar (MML) incluye todos los teoremas a los que los autores pueden hacer referencia en artículos recién escritos. Una vez aprobados por el corrector de pruebas, se evalúan más a fondo en un proceso de revisión por pares para determinar la contribución y el estilo adecuados. Si se aceptan, se publican en el Journal of Formalized Mathematics [10] asociado y se agregan al MML.
Amplitud
En julio de 2012, el MML incluía 1150 artículos escritos por 241 autores. [11] En conjunto, estos contienen más de 10,000 definiciones formales de objetos matemáticos y alrededor de 52,000 teoremas probados en estos objetos. Más de 180 hechos matemáticos nombrados se han beneficiado de la codificación formal. [12] Algunos ejemplos son el teorema de Hahn-Banach , el lema de Kőnig , el teorema del punto fijo de Brouwer , el teorema de completitud de Gödel y el teorema de la curva de Jordan .
Esta amplitud de cobertura ha llevado a algunos [13] a sugerir a Mizar como una de las principales aproximaciones a la utopía QED de codificar todas las matemáticas básicas en forma verificable por computadora.
Disponibilidad
Todos los artículos de MML están disponibles en formato PDF como artículos del Journal of Formalized Mathematics . [10] El texto completo del MML se distribuye con el verificador Mizar y se puede descargar gratuitamente desde el sitio web de Mizar. En un proyecto reciente en curso [14], la biblioteca también se puso a disposición en un formato wiki experimental [15] que solo admite ediciones cuando son aprobadas por el verificador de Mizar. [dieciséis]
El sitio web de MML Query [11] implementa un potente motor de búsqueda para el contenido de MML. Entre otras habilidades, puede recuperar todos los teoremas de MML probados sobre cualquier tipo u operador en particular. [17] [18]
Estructura lógica
El MML se basa en los axiomas de la teoría de conjuntos de Tarski-Grothendieck . Aunque semánticamente todos los objetos son conjuntos , el lenguaje permite definir y usar tipos sintácticos débiles . Por ejemplo, se puede declarar que un conjunto es de tipo Nat sólo cuando su estructura interna se ajusta a una lista particular de requisitos. A su vez, esta lista sirve como definición de los números naturales y el conjunto de todos los conjuntos que se ajustan a esta lista se denota como NAT . [19] Esta implementación de tipos busca reflejar la forma en que la mayoría de los matemáticos piensan formalmente en los símbolos [20] y así simplificar la codificación.
Comprobador de prueba de Mizar
Las distribuciones de Mizar Proof Checker para todos los principales sistemas operativos están disponibles gratuitamente para su descarga en el sitio web de Mizar Project. El uso del comprobador de pruebas es gratuito para todos los fines no comerciales. Está escrito en Free Pascal y el código fuente está a disposición de todos los miembros de la Asociación de Usuarios de Mizar. [21]
Ver también
- Isar (Isabelle)
- Metamath
Referencias
- ^ a b Naumowicz, Adam; Artur Korniłowicz (2009). "Una breve descripción de Mizar". Demostración de teoremas en lógicas de orden superior . Apuntes de conferencias en Ciencias de la Computación. 5674 : 67–72. doi : 10.1007 / 978-3-642-03359-9_5 . ISBN 978-3-642-03358-2.
- ^ a b Wiedijk, Freek (2009). "Formalización del teorema de Arrow" . Sādhanā . 34 (1): 193–220. doi : 10.1007 / s12046-009-0005-1 . hdl : 2066/75428 .
- ^ Matuszewski, romano; Piotr Rudnicki (2005). "Mizar: los primeros 30 años" (PDF) . Matemática mecanizada y sus aplicaciones . 4 .
- ^ Wiedijk, Freek. "Mizar" . Consultado el 24 de julio de 2018 .
- ^ Discusión de la lista de correo Archivado el 9 de octubre de 2011 en la Wayback Machine en referencia a la contratación cercana de Mizar.
- ^ Anuncio de la lista de correo que se refiere al código abierto de MML.
- ^ Geuvers, H. (2009). "Asistentes de prueba: Historia, ideas y futuro" . Sadhana . 34 (1): 3–25. doi : 10.1007 / s12046-009-0001-5 .
- ^ Wiedijk, Freek (2008). "Prueba formal - Introducción" (PDF) . Avisos del AMS . 55 (11): 1408-1414.
- ^ Wiedijk, Freek. "El" factor de Bruijn " " . Consultado el 24 de julio de 2018 .
- ^ a b Diario de matemáticas formalizadas
- ^ a b El motor de búsqueda de consultas MML
- ^ "Una lista de teoremas nombrados en el MML" . Consultado el 22 de julio de 2012 .
- ^ Wiedijk, Freek (2007). "El Manifiesto QED revisado" . De la percepción a la prueba: Festschrift en honor a Andrzej Trybulec . Estudios de Lógica, Gramática y Retórica . 10 (23).
- ^ La página de inicio del proyecto MathWiki
- ^ El MML en forma wiki
- ^ Alama, Jesse; Kasper Brink; Lionel Mamane; Josef Urban (2011). "Grandes wikis formales: problemas y soluciones". Matemática informática inteligente . Apuntes de conferencias en Ciencias de la Computación. 6824 : 133-148. arXiv : 1107.3212 . doi : 10.1007 / 978-3-642-22673-1_10 . ISBN 978-3-642-22672-4.
- ^ Un ejemplo de una consulta MML , que produce todos los teoremas probados en eloperador exponente , por el número de veces que se citan en los teoremas posteriores.
- ^ Otro ejemplo de una consulta MML , que produce todos los teoremas probados en campos sigma .
- ^ Grabowski, Adam; Artur Kornilowicz; Adam Naumowicz (2010). "Mizar en pocas palabras" . Revista de razonamiento formalizado . 3 (2): 152–245.
- ^ Taylor, Paul (1999). Fundamentos prácticos de las matemáticas . Prensa de la Universidad de Cambridge . ISBN 9780521631075. Archivado desde el original el 23 de junio de 2015 . Consultado el 24 de julio de 2012 .
- ^ Sitio web de la Asociación de Usuarios de Mizar
enlaces externos
- Página web oficial