Welche mathematischen Probleme können mit automatisierten Theoremprüfern gelöst werden?

Kann ich folgende Aussagen mit verfügbaren automatisierten Theoremprüfern nachweisen?

$(a+b)^2=a^2+b^2+2ab$ .
Wenn , dann . $11 \mid 2a-3b$ $11 \mid 7a-5b$
Wenn , dann ist . $ax^2+bx+c=0$ $x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$
Wenn ist, ist gerade. $a$ $4a$

und so weiter!

Ich stelle diese Frage, weil ich gerade die Anwendung automatisierter Theorembeweiser gefunden habe, um Theoreme in der Logik zu beweisen.

automated-theorem-proving Mathe-Fort
quelle

Sie können alle diese (außer vielleicht 3, was wie geschrieben falsch ist) mit allen Standard-Proof-Assistenten beweisen, obwohl es wahrscheinlich nicht automatisch sein wird.

Yuval Filmus

@YuvalFilmus. Vielen Dank! Welche Probleme können also automatisch gelöst werden?

Mathe-Fort

Sie können Ausdrücke automatisch vereinfachen, obwohl dies ein Service von Computer Algebra Systems ist. Ich denke nicht, dass moderne Proofassistenten automatisch irgendetwas von Substanz beweisen können, obwohl es besser ist, die Experten zu befragen.

Yuval Filmus

@YuvalFilmus Ich denke, dass das, was Sie sagen, oft wahr ist, in dem Sinne, dass wir es nur dann als Teil eines CAS bezeichnen, wenn eine automatisierte Beweismethode interessante Ergebnisse liefert ...

Diskrete Eidechse

"(a + b) ^ 2 == a ^ 2 + b ^ 2 + 2ab" auf WolframAlpha

Nat

Antworten:

Die meisten Ihrer Aussagen sind elementare Algebra, so dass diese von einem Computeralgebrasystem (CAS) wie Maple oder Mathematica automatisch bewiesen werden können.

(Falls Sie sich für die Mathematik hinter CAS interessieren, kann ich das Buch Modern Computer Algebra von Joachim von zur Gathen und Jürgen Gerhard empfehlen , ein schönes Buch, das als "Bibel" des Fachs gilt.)

Das automatisierte Beweisen von Theoremen ist in der Regel eine heuristische Suche nach einer Struktur, die Beweise darstellt, wenn der Beweis nicht einer der wenigen Fälle ist, für die es einen Algorithmus gibt, der ihn endgültig lösen kann. Da diese Aussagen nicht sehr kompliziert sind, ist es wahrscheinlich, dass ein automatisierter Prüfer in der Lage ist, einen Beweis zu finden.

Ich halte es jedoch für interessant, etwas mehr über die Aussagen zu sagen, für die es nette Algorithmen gibt:

Aussage 3 ist (ein sehr einfacher Fall von) über die Wurzeln eines (Polynom-) Gleichungssystems und kann gelöst werden, indem mit dem Buchberger-Algorithmus eine Gröbner-Basis gefunden wird . Die Gröbner-Basis und der Buchberger-Algorithmus zum Auffinden eines solchen Satzes sind sehr nützliche Werkzeuge zum automatisierten Beweis von Theoremen. Zum Beispiel können wir elementare Theoreme in der Geometrie sogar automatisch beweisen, indem wir das Problem automatisch auf clevere Weise transformieren, um eine Wurzel einer Polynomgleichung zu finden!

Eine weitere interessante Klasse von Theoremen sind Aussagen, die in der quantifiziererfreien Presburger-Arithmetik ausgedrückt werden können (insbesondere ist diese Arithmetik ohne Multiplikation, dies gilt also nicht für Ihre Aussagen), da es einen Algorithmus gibt, mit dem alle derartigen Aussagen gelöst werden können, obwohl der Algorithmus ist ein bisschen langsam.

Diskrete Eidechse
quelle