Esta es la impresión que obtuve al leer el libro de Douglas Hofstadter, Godel, Escher, Bach. Habló de poder diseñar un comprobador de pruebas que aplicara axiomas y teoremas para determinar si se seguía una afirmación de los anteriores. Me recordó a usar BNF para verificar la sintaxis de las declaraciones en un lenguaje de programación.
Respuesta
¿Demasiados anuncios?
MJD
Puntos
37705
¿Has visto metamath ? Es una formalización de una gran cantidad de matemáticas en un sistema extremadamente simple:
Metamath usa una única regla de sustitución simple que le permite seguir cualquier prueba mecánicamente.
Las reglas de deducción son tan simples que pueden ser (y son) verificadas por computadora.
