Ich lerne die automatische Theoremprüfung / SMT-Löser / Proof-Assistenten selbst und stelle hier eine Reihe von Fragen zum Prozess.
Beachten Sie, dass diese Themen ohne Hintergrundwissen in (mathematischen) Logik nicht einfach zu verarbeiten sind. Wenn Sie Probleme mit grundlegenden Begriffen haben, lesen Sie diese nach, z. B. Logik in der Informatik von M. Huth und M. Ryan (insbesondere Kapitel eins, zwei und vier) oder Eine Einführung in die mathematische Logik und Typentheorie von P. Andrews.
Eine kurze Einführung in die Logik höherer Ordnung (HOL) finden Sie hier .
Ich sah Coq an und las unter anderem das erste Kapitel der Einführung zu Isabelle . Arten von automatisierten Theoremprüfern
Ich kenne Prolog seit ein paar Jahrzehnten und lerne jetzt F #, also sind ML, O'Caml und LISP ein Bonus. Haskell ist ein anderes Tier.
Ich habe folgende Bücher
"Handbook of Automated Reasoning", herausgegeben von Alan Robinson und Andrei Vornkov
"Handbuch der praktischen Logik und des automatisierten Denkens" von John Harrison
"Term Rewriting and All That" von Franz Baader und Tobias Nipkow
Was sind die Unterschiede zwischen Coq und Isabelle?
Soll ich entweder Isabelle oder Coq oder beides lernen?
Hat es einen Vorteil, zuerst Isabelle oder Coq zu lernen?
Die nächste Frage der Serie finden Sie hier .
quelle
Antworten:
Ich bevorzuge Coq, aber ich stelle mir vor, dass andere Isabelle bevorzugen. Eines der seltsamen Dinge, die ich an Isabelle gefunden habe, ist, dass es eine zweistufige Syntax gibt, bei der einige Ihrer Definitionen in doppelten Anführungszeichen stehen müssen. Kein solcher Unsinn ist in Coq vorhanden.
Letztendlich hängt die für Sie am besten geeignete davon ab, was Sie beweisen möchten. Beide Sprachen verfügen über umfangreiche Bibliotheksunterstützung und aktive Communities, die alle Arten von Entwicklungs- und Beispieltheorien ausführen. Wenn eine Sprache eine ausreichende Unterstützung für die Bibliothek (oder eine andere) für die Art von Theorie bietet, die Sie entwickeln möchten, dann würde ich diese Sprache auswählen.
Eine Strategie besteht darin, ein einfaches Tutorial in beiden Sprachen zu erstellen und das zu befolgen, das sich am besten anfühlt. Zum Beispiel,
Hier ist ein Blog-Beitrag, in dem jemand kurz die beiden miteinander vergleicht, der letztendlich Isabelle bevorzugt.
Stellen Sie sicher, dass Sie eine richtige IDE (wie ProofGeneral ) verwenden, anstatt Dinge auf der Befehlszeile auszuführen .
Eine andere Möglichkeit, in Coq einzusteigen, ist das Online-Buch Software Foundations von Benjamin Pierce et al. Es bietet ein exzellentes Tutorial mit vielen Details. Der Schwerpunkt liegt hauptsächlich auf der Programmiersprachensemantik, aber viele der Grundlagen (und darüber hinaus) der Coq- und halbautomatischen Theoremprüfung werden auf diesem Weg behandelt.
quelle
Eine Sache, die Sie meiner Meinung nach interessant finden werden, ist, dass der Begriff "Theorem Beweis" sehr unterschiedlich ist, je nachdem, in welchem Bereich Sie sich befinden (siehe ausführlich im Handbuch des automatisierten Denkens) hat weniger mit Coq oder Isabelle zu tun, als man denkt.
Als ich mich zum ersten Mal auf den Weg machte, um etwas über das Prüfen von Theoremen zu lernen, war das erste Buch, das ich las (obwohl es jetzt ziemlich alt ist?), Melvin Fittings ausgezeichnete Logik erster Ordnung und automatisierte Theoremprüfung. Dieses Buch war wirklich exzellent und behandelte die Arten von Themen, die Sie im Zusammenhang mit der Logik niedrigerer Ordnung sehen werden, wo Sie tatsächlich ein gutes Maß an Automatisierung erhalten können. Die Art von Logik, die Sie lernen, sollte von dem diktiert werden, worüber Sie argumentieren möchten, und nicht so sehr von dem Satz, der sich dafür als nützlich erweist. Zum Beispiel, während Logik erster Ordnung Ihnen ein gutes Maß an Ausdruckskraft und Denkvermögen verleiht, hat sich der Großteil der Programmiersprachen-Community (in der ich in diesen Tagen gelandet bin) von der älteren Schule der Theorembeweisung und Modellprüfung (auf die wir eingehen) verabschiedet der Eimer mit Dingen, die entscheidender, aber weniger aussagekräftig sind).
Das soll jedoch nicht heißen, dass Dinge wie Argumentation erster Ordnung und Modellprüfung in der Praxis nicht besonders nützlich waren. Sie waren! Sie können sich ACL2 als Beispiel für einen Prover ansehen, der auf Logik erster Ordnung aufgebaut ist und im industriellen Bereich erstaunliche Erfolge erzielt hat. Daneben hat sich auch das Lösen von SMT erstaunlich stark weiterentwickelt. Moderne SMT-Solver bauen auf sehr leistungsfähigen SAT-Solvern auf (meistens durch Entdeckungen in den letzten zwanzig Jahren zur Verbesserung von DPLL) und haben in Dingen wie der symbolischen Ausführung eine große Verwendung erfahren.
Wie ich bereits sagte, macht das traditionellere "Theorem-Beweisen" zwar Spaß, aber es gibt noch viel mehr zu lernen. Das Erlernen von Coq zum Beispiel hat wenig mit dem Erlernen der Automatisierungswerkzeuge zu tun, die es Ihnen gibt, und hat viel mehr mit dem Erlernen der Typentheorie zu tun, auf der es basiert (der prädikativen Berechnung von coinduktiven Konstruktionen). Wenn Sie nicht an konstruktive Logik, Curry-Howard-Isomorphismus oder Typentheorie gewöhnt sind, werden Sie eine aufregende Zeit damit verbringen, diese Werkzeuge zu erlernen, aber ich kann kaum glauben, dass sie zu eng mit den Dingen zusammenhängen, die Sie im ersten Band sehen des Handbuchs.
Entscheiden Sie also, was Sie tun möchten: Überprüfen Sie Modelle und Theoreme in der Logik erster Ordnung oder verwenden Sie eine leistungsstarke Typentheorie, um über die Richtigkeit Ihrer Programme (oder Theoreme in der konstruktiven Logik) zu urteilen. Wenn es das erste ist, lernen Sie mehr über automatisierte deduktionsbasierte Techniken, wenn es das zweite ist, lernen Sie mehr über Coq, HOL, etc ... Übrigens, wenn Sie Coq lernen möchten, während die obigen Referenzen gut sind, denke ich, dass Es gibt zwei wirklich wichtige Referenzen für das Lernen von Coq:
Benjamin Pierces Software-Grundlagenbuch (Dr. Pierce ist ein ausgezeichneter Autor, und ich würde empfehlen, dass Sie sich auch sein populäreres "Ziegelbuch" ansehen, wenn Sie es noch nicht getan haben).
Zertifizierte Programmierung mit abhängigen Typen (Adam Chlipala schreibt auch recht gut, obwohl seine Bücher etwas reifer und intelligenter sind als Pierces vielleicht einfachere Einführung.)
quelle
Es gibt eine Vielzahl von Systemen für Interactive Theorem Proving (ITP) - siehe auch die Konferenz mit diesem Namen - Coq, Isabelle, HOLs, ACL2, PVS usw.
Alle von ihnen sind relativ schwierig zu lernen, und jeder hat seine eigene spezifische Kultur. Es ist wie das Erlernen einer Fremdsprache: Nehmen wir an, Sie sprechen bereits Englisch und haben dann die Wahl zwischen Französisch, Deutsch, Italienisch, Spanisch und Portugiesisch. Alle sind irgendwie verwandt - das sind keine Chinesen - aber nur sehr wenige Leute schaffen das alles gleichzeitig. Also sollten Sie versuchen, einen Vorgeschmack auf die einzelnen Kulturen und Gemeinschaften zu bekommen und dann eine Verpflichtung eingehen.
Möglicherweise gibt es auch die "Killer-Funktion", die Sie wirklich für Ihre Arbeit benötigen.
Es ist auch hilfreich, Experten für eines dieser Systeme zu haben.
Beide sind Nachkommen des LCF-Systems aus Stanford / Edinburgh / Cambridge. 1985 arbeiteten G. Huet und L. Paulson gemeinsam an der letzten Version von Cambridge LCF. Dann geschah die Trennung in Richtung Coc / CIC / COQ (jetzt Coq) in Frankreich und Isabelle in Cambridge und München. Beachten Sie, dass HOL4, HOL-Light, HOL-XYZ andere verwandte Nachkommen von LCF sind.
Vor mehr als 20 Jahren wäre die Unterscheidung von Coq und Isabelle nach logischen Grundsätzen getroffen worden: Abhängig typisierte konstruktive Logik hier, einfach typisierte klassische Logik dort. Heutzutage hat dies in der Praxis überraschend wenig Auswirkungen, da mehr und mehr Ebenen zu jedem formalen System hinzugefügt wurden, einschließlich Zusatztools und Bibliotheken.
Sie sollten sich beide ansehen und versuchen, ein Gefühl dafür zu bekommen, ob Sie mehr Wein und Käse oder Bratwurst und Sauerkraut mögen. (Als einer der Jungs hinter Isabelle, aber derzeit in Frankreich, wundere ich mich, wie viele Franzosen Sauerkraut wirklich mögen, wenn sie privat zu Hause sind und niemand hinschaut :-)
Ich glaube nicht. Es besteht die Gefahr, dass Sie bei dem einen hängen bleiben, den Sie zuerst versuchen, und nicht bei dem zweiten, oder dass Sie bei dem ersten zu früh enttäuscht werden und ihn zu früh abweisen. In jedem Fall benötigen Sie Zeit und Ausdauer, um mit beiden Systemen produktiv zu werden.
Da Proof General als "IDE" bereits erwähnt wurde: Proof General / Emacs war über viele Jahre die einheitliche Standardschnittstelle für Coq und Isabelle, aber ich hätte es nie eine IDE genannt. Es gibt auch CoqIDE mit dem Namen "IDE", aber es ist ein relativ einfacher Editor über Gtk-Widgets. Die aktuelle Version von Isabelle enthält Isabelle / jEdit, das nicht "IDE" im Namen hat, sondern dazu gedacht ist, Dinge zu approximieren, die Sie routinemäßig in Netbeans oder IntelliJ IDEA sehen - für Proof-Texte anstelle von Java-Code.
quelle
Hier sind ein paar nette Video-Coq-Tutorials von Andrej Bauer. Es ist in keiner Weise vollständig, aber ich denke, es ist eine gute Einführung.
quelle
Diese Einführung in Isabelle ist ziemlich vollständig.
Siehe auch diese Einführung zu Isabelle
Im Allgemeinen ist Isabelle relativ einfach zu starten, da es viele verfügbare Beispiele gibt. Zum Beispiel auf der offiziellen Website
PS - Ich bin in keiner Weise mit Isabelle verbunden, ich bin ein Theoretiker in formalen Methoden, aber ich weiß, dass Isabelle oft als Standardausgangspunkt auftaucht.
quelle
Ich bin kürzlich zu diesen Coq-Tutorials aus conf2017 gekommen, daher habe ich herausgefunden, dass es sich lohnt, sie hier für alle zu teilen, die diese Frage später besuchen.λ
Die Software Foundations der DeepSpec Summer School bieten auch einige ziemlich coole Vorträge:
Einige der Vorlesungen, die auf der Software-Grundlagenreihe basieren, wurden bereits erwähnt.
Coq Intensiv
Verifizierte Funktionsalgorithmen
quelle