To może być uznane za głupie pytanie. Nie jestem informatyką (i jeszcze nie jestem matematyką), więc przepraszam, jeśli uważasz, że poniższe pytania zawierają pewne błędne założenia.
Chociaż istnieją plany sformalizowania ostatniego twierdzenia Fermata (patrz ta prezentacja ), nigdy nie czytałem ani nie słyszałem, że komputer może udowodnić nawet „proste” twierdzenie takie jak Pitagoras ”.
Dlaczego nie? Jaka jest (są) główna trudność (trudności) w ustanowieniu w pełni autonomicznego dowodu przez komputer, wspomagany tylko przez niektóre „wbudowane aksjomaty”?
Drugie pytanie, które chciałbym zadać, brzmi: dlaczego jesteśmy w stanie sformalizować wiele dowodów, podczas gdy komputer nie jest w stanie samodzielnie udowodnić twierdzenia? Dlaczego to „trudniejsze”?
źródło
Odpowiedzi:
W 1949 r. Tarski udowodnił, że prawie wszystko w Elementach mieści się w rozstrzygającym fragmencie logiki, gdy wykazał rozstrzygalność teorii pierwszego rzędu rzeczywistych zamkniętych pól. W szczególności twierdzenie Pitagorasa nie mówi zbyt wiele, ponieważ nie jest szczególnie trudne.
źródło
Dwie główne trudności. Niekompletność (patrz Twierdzenia o niekompletności Gödla) i ogromna wielkość przestrzeni poszukiwań (jest znacznie więcej nieciekawych twierdzeń niż ciekawych). Osiągnięto znaczny postęp dzięki asystentom dowodowym ( Coq , Isabelle, Agda itp.). Za ich pomocą matematyk pisze twierdzenia i lematy, a asystent dowodu pomaga znaleźć dowody i zapewnia ich logiczną ważność.
W tym artykule opisano, w jaki sposób stosuje się asystenta dowodu Coqa do udowodnienia twierdzenia o czterech kolorach. Matematyka zmechanizowana ( przegląd ) jest jednym z obszarów TCS poświęconym (częściowo) automatycznemu dowodzeniu twierdzeń (i na ogół używaniu komputerów do pomocy matematykom).
Jednym z obszarów, w którym automatyczne dowodzenie twierdzeń (swego rodzaju) ma wpływ, jest sprawdzanie i znajdowanie modeli. Sprawdzanie modelu zajmuje się określaniem, czy dany system spełnia daną właściwość, podczas gdy wyszukiwanie modelu znajduje system spełniający daną kolekcję właściwości. Narzędzie Alloy wykorzystuje sprawdzanie modeli i znajdowanie modeli z dobrym skutkiem i jest całkiem użyteczne.
źródło