Gibt es ein vernünftiges automatisiertes Beweissystem für TCS-Theoreme?

28

Angenommen, ich wollte Turings Beweis für das Stopp-Problem formalisieren, damit eine Maschine ihn überprüfen kann. Einige der bekannten automatisierten Theoremprüfungssysteme umfassen Mizar, Coq und HOL4. Ich habe Coq heruntergeladen und experimentiert, aber es gibt keine Bibliothek für Turing-Maschinen. Ich überlegte, selbst einen Code zu schreiben, fand das Tutorial jedoch nicht ausreichend und die Sprache schwer zu erlernen.

Meine Frage ist: Gibt es einen automatisierten Theorembeweiser, der Theoreme mit Turing-Maschinen im Allgemeinen gut beweisen kann? Ich würde einen solchen Theorembeweis als "gut" betrachten, wenn er einen Beweis für die Unentscheidbarkeit des Halteproblems unter Verwendung bereits vorhandener Bibliotheken formulieren kann. Ich würde es sogar noch besser finden, wenn es relativ einfach zu erlernen ist. (Ich habe normalerweise keine Schwierigkeiten mit Programmiersprachen.)

Vielen Dank,

Philip

lo.logic turing-machines software proof-assistants automated-theorem-proving Philip White
quelle
Möglicherweise möchten Sie diese Seite überprüfen , die Liste enthält jedoch nicht das Problem mit dem Anhalten.
Kaveh
10
Ich wage zu sagen, dass Sie mit so etwas wie Coq bestehen müssen, bevor es sich natürlich anfühlt. Und Sie müssen am Terminal sein, um Probleme zu lösen, anstatt das Buch zu lesen. Wenn Sie sich mit "Interaktives Beweisen von Theoremen und Programmentwicklung: Coq'Art: Die Berechnung induktiver Konstruktionen" vertraut machen, ist dies hilfreich. Coq-Tutorials: cis.upenn.edu/~bcpierce/sf und adam.chlipala.net/cpdt sind ziemlich gut (obwohl sie nicht direkt auf das ausgerichtet sind, was Sie wollen).
Dave Clarke
5
Die Formalisierung eines Beweises kann ziemlich kompliziert sein, wenn Sie die "falsche" Version davon auswählen. Für das Halting-Problem würde ich vorschlagen, zuerst eine allgemeinere und abstraktere Version zu beweisen. Dann können Sie später nachweisen, dass Turing-Maschinen ein Sonderfall der abstrakten Version sind, wenn Sie immer noch Lust dazu haben (es gibt sehr viele langweilige Details zu Turing-Maschinen, daher ist es vielleicht besser, etwas anderes zu tun). Ich werde mir überlegen, wie ich das in Coq beweisen kann. Ich blieb dran.
Andrej Bauer
5
Wenn Sie gut in Mathematik und in Programmierung sind, haben Sie die Voraussetzungen, um den Umgang mit einem Proof-Assistenten zu erlernen. Sie müssen es wirklich als eine neue Fähigkeit behandeln. (Es ist jedoch sehr lohnend.)
Neel Krishnaswami
Die Antwort auf die Frage scheint "nein" zu sein. Ein solches System wäre meiner Meinung nach sehr nützlich. Darf ich Sie bitten, bei der Formalisierung von Turing-Maschinen ein wenig über die Polynom-Zeit-Äquivalenz nachzudenken?
Colin McQuillan

Antworten:

17

Hier ist eine Isabelle / HOL-Bibliothek, die den Satz von Rice enthält und die Unentscheidbarkeit einer Vielzahl von Problemen angibt. Da diese Bibliothek die Berechenbarkeit über rekursive Funktionen modelliert, müssen Sie eine universelle Turing-Maschine als rekursive Funktion codieren, um mit diesem Theorem die Unentscheidbarkeit des Halteproblems von Turing-Maschinen zu beweisen. Die wesentlichen Teile des Unentscheidbarkeitsnachweises sind jedoch bereits erledigt.

http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html

yhirai
quelle