Soy asistente de pruebas de autoaprendizaje y decidí comenzar con algunas pruebas básicas y progresar. Como las pruebas se basan en otras pruebas y, por lo tanto, forman una jerarquía, ¿existe un depósito de la jerarquía de pruebas?
Sé que puedo elegir un asistente de pruebas en particular y analizar su biblioteca para extraer su jerarquía, sin embargo, si quiero encontrar la siguiente prueba en una cadena para probar, no puedo cuando no está en la biblioteca.
En mi opinión, imagino un gráfico, probablemente un DAG , de todas las pruebas matemáticas conocidas que se pueden expresar usando declaraciones en inglés, no pruebas usando imágenes . Este sería el mapa maestro (un mapa en el sentido de comenzar en un punto y viajar a otro punto a través de puntos intermedios), y para un asistente de prueba particular, uno tendría un subgrafo del mapa maestro. Luego, si uno quisiera crear una prueba usando un asistente de prueba que se encuentra en el maestro y no en el subgrafo, al comparar los dos gráficos se podría tener una idea del trabajo necesario para crear las pruebas que faltan para el asistente de prueba.
Soy consciente de que las pruebas matemáticas no son necesariamente fáciles de usar para un asistente de pruebas, sin embargo, tener una idea general de qué hacer es mucho mejor que ninguna.
Además, al tener el mapa maestro, puedo ver si hay múltiples rutas de un punto a otro y elegir una ruta que sea más adecuada para el asistente de prueba particular.
EDITAR
Al buscar encontré algo similar para las funciones matemáticas . No encontré uno para pruebas en el NIST
fuente
Respuestas:
El sistema Mizar es un gran depósito de pruebas matemáticas. Vea la página de wikipedia y el sitio web oficial .
De wikipedia / Mizar_system # Mizar_language :
Las pruebas se escriben como artículos, de los cuales hay más de mil artículos y más de 50,000 teoremas probados. La página de wikipedia menciona algunas ideas interesantes del " manifiesto QED ", y cómo Mizar podría estar en camino de lograr esto.
fuente
ProofWiki contiene una cantidad decente de pruebas de varias áreas de las matemáticas. De ninguna manera está completo, pero es un buen punto de partida para lo que desea.
fuente
Metamath tiene una gran selección de pruebas, construidas desde su núcleo en lógica proposicional.
Dicho esto, carece dolorosamente en términos de teoría CS. ¡Siéntase libre de expandirlo!
fuente
Vea el archivo TPTP , Miles de problemas para los probadores de teoremas. Es algo estándar en el campo. Estos son más los "nodos" del gráfico del teorema sobre el que está preguntando. Algunos documentos que se refieren al archivo pueden haber explorado los bordes en este gráfico.
Tenga en cuenta que en el campo de la ATM, la prueba de teorema automatizada y la prueba de teorema asistida, las pruebas son simbólicas y no es realmente factible o plausible estudiar "pruebas en inglés" mientras visualiza.
Sin embargo, puede aprender sobre la paradoja de Richard, que comenzó como una formulación de lenguaje y luego se formalizó simbólicamente. Se dice que es la inspiración para los "antimonios" (contradicciones) encontrados en la teoría de conjuntos temprana que históricamente incluso allanó el camino al teorema de incompletitud de Gödel.
fuente