Hace algún tiempo leí algunos artículos sobre formalización de pruebas. Por lo general, comencé con este , desde Lamport.
¿Hay trabajos más recientes en este campo?
Respuestas
¿Demasiados anuncios?
Tom Feiner
Puntos
2899
Hubo un número especial de los avisos del AMS sobre formal proof en 2008. Freek Wiedijk, quien escribió uno de los artículos de Notices, tiene algunos buenos recursos en su página de inicio .
En general, "la formalización matemática lengua vernácula" es una buena fuente de trabajo correspondiente a su pregunta. El campo generalmente se inició formalmente con la de Bruijn del Automath proyecto.
Harvey Friedman ha hecho un buen trabajo en el aprovechamiento de su teoría de las definiciones explícitas de la teoría de conjuntos (cf. La Lógica de la Fuerza de los enunciados Matemáticos I, 1976) para dar un idioma para hacer matemáticas de una manera que es bastante natural, y que puede ser fácilmente traducido a pruebas de más de ZFC.
Me temo que no tengo una buena referencia para esto: en que él dio una charla a la ASL conferencia de 2006, en Nijmegen.
Postscript
Me acordé de allí fueron coautores: el sistema fue escrito en una serie de documentos para un sistema que se llama Un lenguaje para la gestión del conocimiento, debido a Steve Kieffer (para un proyecto de Maestría), Jeremy Avigad, y Harvey Friedman.
Renaud Bompuis
Puntos
10330
Hay un Journal of Formalized Mathematics conectado con el proyecto Mizar
