Wenn es einen Weg gibt, einen Proofer für die mathematische Induktion zu implementieren, wie würde er aussehen? Wenn es nicht möglich ist, warum?Automatisiertes Theorem-Proofing für die mathematische Induktion
Ich habe über einen Weg nachgedacht, wo Sie grundlegende Axiome und Regeln als Eingabe spezifizieren und auf Probleme mit grundlegenden Summen und Gleichungen beschränken.
Wäre es für mathematische Beweise im Allgemeinen genauso?
Ich werde die Antwort auf Induktion über die natürlichen Zahlen begrenzt halten.
Lassen Sie S(n) die Aussage sein, die Sie durch Induktion für alle n beweisen möchten. Dann muss das Programm überprüfen: S(0) und S(n) => S(n+1).
Der erste Teil ist so schwer wie der Nachweis einer Aussage, der zweite Teil ist der Nachweis der Äquivalenz zweier solcher Aussagen. Das heißt, auch wenn der erste Teil nicht schwer ist, könnte der zweite Teil NP-hard sein (zu meinem Wissen). Also ja, ein Proofer kann implementiert werden (muss nur die eine Aussage und die Äquivalenz von zwei Aussagen überprüfen), aber ich glaube nicht, dass Sie garantieren können, dass er beendet.
BTW, nicht alle Beweise beginnen von S (0). In vielen Fällen gehen Sie von einer Konstanten aus und nehmen dann für n an und beweisen dann für n + 1. –
@GoodLuck Sie können jeden Beweis von einem konstanten Start von 0 beginnen – WorldSEnder
Mit "Proofer" meinen Sie einen Algorithmus, der einen Beweis für eine gegebene Aussage findet? Turing hat gezeigt, dass das generell nicht möglich ist. Wenn Sie eine Maschine meinen, die Beweise basierend auf gegebenen Axiomen erzeugt, ist das möglich. Aber die Induktion ist so ein großer Teil der axiomatischen Zahlentheorie, dass fast alle Beweise Induktion auf der einen oder anderen Stufe verwenden. –