Jestem samoukiem, asystentem ds. Dowodów i postanowiłem zacząć od kilku podstawowych dowodów i podążać swoją drogą. Ponieważ dowody są oparte na innych dowodach, a zatem tworzą hierarchię, czy istnieje repozytorium hierarchii dowodów?
Wiem, że mogę wybrać konkretnego asystenta proofów i przeanalizować jego bibliotekę, aby wyodrębnić jego hierarchię, jednak jeśli chcę znaleźć kolejny dowód w łańcuchu do udowodnienia, nie mogę, gdy nie ma go w bibliotece.
Moim zdaniem wyobrażam sobie wykres, prawdopodobnie DAG , wszystkich znanych matematycznych dowodów, które można wyrazić za pomocą angielskich stwierdzeń, a nie dowodów za pomocą obrazów . Byłaby to mapa główna (mapa w sensie rozpoczynania się w jednym punkcie i podróżowania do innego punktu przez punkty pośrednie), a dla konkretnego asystenta dowodu miałby się podgraph mapy głównej. Następnie, jeśli ktoś chciałby stworzyć dowód przy użyciu asystenta dowodu znalezionego na wzorcu, a nie na podsgrafie, porównując dwa wykresy, można uzyskać wyobrażenie o pracy potrzebnej do stworzenia brakujących dowodów dla asystenta dowodu.
Zdaję sobie sprawę, że dowodów matematycznych niekoniecznie łatwo można przekonwertować do użycia z asystentem dowodu, jednak ogólne pojęcie o tym, co należy zrobić, jest znacznie lepsze niż wcale.
Również mając mapę główną, widzę, czy istnieje wiele ścieżek od jednego punktu do drugiego, i wybieram ścieżkę, która jest bardziej odpowiednia dla konkretnego asystenta dowodu.
EDYTOWAĆ
Podczas wyszukiwania znalazłem coś podobnego do funkcji matematycznych . Nie znalazłem jednego na dowód w NIST
źródło
Odpowiedzi:
System Mizar to ogromne repozytorium dowodów matematycznych. Zobacz stronę wikipedii i oficjalną stronę internetową .
Z wikipedia / Mizar_system # Mizar_language :
Dowody są pisane jako artykuły, z których jest ponad tysiąc artykułów i ponad 50 000 udowodnionych twierdzeń. Strona wikipedia wspomina kilka interesujących pomysłów na „ manifest QED ” oraz o tym, jak Mizar może być na drodze do osiągnięcia tego celu.
źródło
ProofWiki zawiera przyzwoitą liczbę dowodów z różnych dziedzin matematyki. Nie jest to bynajmniej kompletne, ale jest dobrym punktem wyjścia do tego, czego chcesz.
źródło
Metamath ma duży wybór dowodów, zbudowanych od samego początku w logice zdań.
To powiedziawszy, boleśnie brakuje w teorii CS. Możesz go rozwinąć!
źródło
Zobacz archiwum TPTP , Tysiące problemów dla dostawców twierdzeń. Jest to nieco standard w tej dziedzinie. To bardziej „węzły” grafu twierdzeń, o które pytasz. Niektóre artykuły odnoszące się do archiwum mogły badać krawędzie na tym wykresie.
Zauważ, że w dziedzinie ATM, automatycznego dowodzenia twierdzeń i dowodzenia twierdzeń wspomaganych dowody są symboliczne i studiowanie „dowodów w języku angielskim” podczas wizualizacji nie jest realne ani wykonalne.
Możesz jednak dowiedzieć się o paradoksie Richarda, który początkowo był sformułowaniem językowym, a później został sformalizowany symbolicznie. Mówi się, że jest inspiracją dla „antymonów” (sprzeczności) znalezionych we wczesnej teorii mnogości, która historycznie nawet utorowała drogę do twierdzenia o niekompletności Gödla.
źródło