¿Hay un depósito de la jerarquía de las pruebas?

Question

Soy de autoaprendizaje y decidieron comenzar en algunas pruebas básicas y trabajar mi camino hacia arriba. Dado que las pruebas se basan en otras pruebas y así forman una jerarquía, ¿hay un repositorio de la jerarquía de las pruebas?

Yo sé que puedo escoger una prueba asistente particular y analizar su biblioteca para extraer su jerarquía, sin embargo si quiero encontrar la siguiente prueba en una cadena de probar, no puedo cuando no está en la biblioteca.

En mi mente me imagino a un gráfico, probablemente un DAG , de todas las pruebas matemáticas conocidas que se pueden expresar el uso de declaraciones en inglés, no utilizando imágenes . Este sería el mapa maestro (un mapa en el sentido de partida en un punto y viajar a otro punto a través de puntos intermedios), y por un asistente de prueba particular, uno tendría un subgrafo del mapa maestro. Entonces, si uno quería crear una prueba usando un asistente prueba se encuentran en el maestro no en el subgrafo, mediante la comparación de los dos gráficos se podría tener una idea de los trabajos necesarios para crear la prueba (s) faltante para el asistente prueba.

Soy consciente de que las demostraciones matemáticas no son necesariamente fácilmente convertible para su uso con un ayudante de la prueba, sin embargo, tener una idea general de lo que debe hacer es mucho mejor que ninguno en absoluto.

También por tener el mapa maestro, que puede ver si hay caminos Mulitple de un punto a antoher y elegir un camino que es más favorable para el asistente prueba particualr.

editar

En la búsqueda he encontrado algo similar para funciones matemáticas . No he encontrado una para pruebas en el NIST

Answer 1

El sistema de Mizar es un enorme repositorio de pruebas de matemáticas. Ver la página de Wikipedia href="http://en.wikipedia.org/wiki/Mizar_system" rel="noreferrer"> y la sitio web oficial .

de todas las pruebas matemáticas conocidas que se pueden expresar mediante declaraciones inglés

Wikipedia / Mizar_system # Mizar_language :

La característica distintiva de la lengua Mizar es su legibilidad

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 de la " QED manifiesto ", y cómo podría ser Mizar en su manera de lograr esto.

• gráfico de la biblioteca Mizar.
• Este documento también puede ser útil: Combinando Mizar y TPTP Semántica Herramientas de presentación

Answer 2

ProofWiki contiene una buena cantidad de pruebas de diversas áreas de las matemáticas. Es de ninguna manera completa, pero es un buen punto de partida para lo que quieres.

Answer 3

Metamath tiene una gran selección de pruebas, ha sido construida desde su base en la lógica proposicional.

Dicho esto, está dolorosamente ausente en términos de la teoría de CS. Siéntase libre para expandirlo!

Answer 4

Vea la TPTP archivo , miles de problemas para teorema Demostrantes. Es algo estándar en el campo. Esto es más los "nodos" de la gráfica teorema usted está planteando. Algunos documentos referentes al archivo pueden haber explorado los bordes en este gráfico.

Tenga en cuenta que en el ámbito de la ATM, demostración automática de teoremas y asistido demostración de teoremas, las pruebas son simbólicas y no es realmente posible o verosímil para estudiar "las pruebas en el idioma Inglés" mientras se visualiza.

Sin embargo, usted puede aprender acerca de paradoja de Richard, que comenzó como una formulación lengua y era más tarde formalizado simbólicamente. Se dice que es la inspiración para "antinomias" (contradicciones) encontrado en la teoría de conjuntos temprano que históricamente incluso abrió el camino a teorema de incompletitud de Gödel.