Jakie problemy matematyczne można rozwiązać za pomocą automatycznych dowodów twierdzeń?

Czy mogę udowodnić następujące stwierdzenia przy użyciu dostępnych automatycznych dowodów twierdzeń?

. $(a+b)^2=a^2+b^2+2ab$
Jeśli , to . $11 \mid 2a-3b$ $11 \mid 7a-5b$
Jeśli , to $ax^2+bx+c=0$ . $x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$
Jeśli jest parzyste, to jest parzyste. $a$ $4a$

i tak dalej!

Zadaję to pytanie, ponieważ właśnie znalazłem zastosowanie zautomatyzowanych dowódów twierdzeń w dowodzeniu twierdzeń w logice.

automated-theorem-proving

— Fort matematyki
źródło

Z pewnością możesz to wszystko udowodnić (może z wyjątkiem 3, co jest niepoprawne, jak napisano) przy użyciu wszystkich standardowych asystentów proof, choć prawdopodobnie nie będzie to automatyczne.

— Yuval Filmus

@YuvalFilmus. Dzięki! Jakie problemy można rozwiązać automatycznie?

— Math-fort

Możesz uprościć wyrażenia automatycznie, chociaż jest to usługa świadczona przez Computer Algebra Systems. Nie sądzę, aby współcześni asystenci dowodowi mogli automatycznie udowodnić coś merytorycznego, chociaż lepiej zapytać ekspertów.

— Yuval Filmus

@YuvalFilmus Myślę, że to, co mówisz, jest często prawdziwe, w tym sensie, że tylko wtedy, gdy zautomatyzowana metoda dowodowa daje interesujące wyniki, jesteśmy skłonni nazwać ją częścią CAS ...

— Dyskretna jaszczurka

„(a + b) ^ 2 == a ^ 2 + b ^ 2 + 2ab” na WolframAlpha

— Nat

Większość twoich wypowiedzi to algebra elementarna, więc można to udowodnić automatycznie za pomocą komputerowego systemu algebry (CAS), takiego jak Maple lub Mathematica.

(Jeśli interesujesz się matematyką stojącą za CAS, mogę polecić książkę Modern Computer Algebra Joachima von zura Gathena i Jürgena Gerharda, piękną książkę, uważaną za „biblię” tej dziedziny)

Zautomatyzowane dowodzenie twierdzeń zwykle polega na przeszukiwaniu heurystycznym struktury reprezentującej dowody, jeśli dowód nie jest jednym z niewielu przypadków, dla których istnieje algorytm, który może go jednoznacznie rozwiązać. Biorąc pod uwagę, że te stwierdzenia nie są zbyt skomplikowane, prawdopodobne jest, że automatyczny dowodzący jest w stanie „znaleźć” dowód.

Myślę jednak, że warto powiedzieć nieco więcej o instrukcjach, dla których istnieją ładne algorytmy:

Stwierdzenie 3 jest (bardzo prosty przypadek) o pierwiastkach (układu) równań wielomianowych i można je rozwiązać poprzez znalezienie podstawy Gröbnera za pomocą algorytmu Buchbergera. Podstawa Gröbnera i algorytm Buchbergera do znalezienia jednego są bardzo fajnymi narzędziami do automatycznego dowodzenia twierdzeń. Na przykład możemy nawet automatycznie udowodnić elementarne twierdzenia w geometrii, automatycznie przekształcając problem do znalezienia pierwiastka równania wielomianowego w sprytny sposób!

Kolejną interesującą klasą twierdzeń są wyrażenia wyrażone w wolnej od kwantyfikacji arytmetyce Presburgera (w szczególności ta arytmetyka jest bez mnożenia, więc nie dotyczy to twoich instrukcji), ponieważ istnieje algorytm do rozwiązania wszystkich takich instrukcji, mimo że algorytm jest trochę wolny.

— Dyskretna jaszczurka
źródło