Warum brauchen einige Inferenz-Engines menschliche Hilfe, andere nicht?

^{Ich lerne die automatische Theoremprüfung / SMT-Löser / Proof-Assistenten selbst und stelle hier eine Reihe von Fragen zum Prozess .}

Warum benötigen automatisierte Theorembeweiser, dh ACL2- und SMT-Löser, keine menschliche Unterstützung, während Beweisassistenten, dh Isabelle und Coq , dies tun?

^{Die nächste Frage der Serie finden Sie hier .}

Gültigkeit höherer Ordnung Formeln ist in der Regel nicht entscheidbar und suchen Räume sind riesig , so alles , was Sie zu tun , hoffen kann , ist zu versuchen , einen Beweis zu finden - vorausgesetzt , es existiert - durch geschickte den Beweis Raum aufzählt (denken Vorschlaghammer , treffend benannt) aber das ist rau. Menschen können das Orakel spielen, indem sie die Schlüssellemmata bereitstellen, um den Beweis zu führen.

Auf der anderen Seite beschäftigen sich automatisierte Prüfer normalerweise nur mit entscheidbaren (Teil-) Logiken, zum Beispiel Aussagenlogik oder Unterklassen von Logik erster Ordnung, so dass sie eine lange Zeit ausgeführt werden können, aber Sie wissen, dass sie irgendwann erfolgreich sein werden.

Beachten Sie, dass es Ansätze gibt, mit denen Proofassistenten wichtige Lemmata finden können, z . B. IsaPlanner . Das Tool schätzt (induktive) Lemmata durch Aufzählung und zufällige Prüfung und versucht dann, sie zu beweisen. Durch die Iteration des Prozesses können viele Lemmata von beispielsweise typischen Datentypdefinitionen automatisch gefunden werden.

Kleines ABC

• Gültigkeit - Eine Formel ist gültig und enthält alles, was Sie den freien Variablen zuweisen.
• freie Variablen - die Variablendie nicht von quantifiers wie gebunden sind und$\forall$$\exists$
• Entscheidbarkeit - Eine (boolesche) Eigenschaft ist (Turing) entscheidbar, wenn es einen Algorithmus gibt, der nach einer begrenzten Zeit mit "Ja" oder "Nein" (richtig) antwortet.
• Aussagenlogik - auch Logik nullter Ordnung ; keine Quantifizierung erlaubt.
• $\forall x. P(x)$$\forall f. f(4) > 0$
• Logik höherer Ordnung - Sie können beliebig komplexe Objekte quantifizieren (und "bauen"), z. B. Funktionen höherer Ordnung (Funktionen, die Funktionen übernehmen).

Ich würde sagen, dass die klassische Unterscheidung von "automatisierten Theoremprüfungen" (ATP) und "interaktiven Theoremprüfungen" (ITP) überdacht werden muss. Wenn Sie heute ein bekanntes ITP-System wie Isabelle / HOL verwenden (Isabelle2013 ab Februar 2013), sind zahlreiche Zusatztools aus dem ATP-Portfolio integriert:

• Integrierte generische automatisierte Proof-Tools: Isabelle-Tools der alten Schule wie fastund blast(von L. Paulson) und neuere automatisierte Tester wie metis(von J. Hurd).

• Externe ATPs für Logik erster Ordnung, die über Vorschlaghammer aufgerufen werden: E Prover, SPASS, Vampire. Der gefundene Beweis wird analysiert, um herauszufinden, welche Lemmas dazu beigetragen haben. Dabei werden 10000s auf 10s reduziert und das Ergebnis an weitergeleitet metis.

• Externe SMTs mit partieller Beweisrekonstruktion, insbesondere für Z3 (von S. Boehme).

• Werkzeuge, um Gegenbeispiele für unbewiesene Aussagen zu finden: Nitpick / Kodkodi (J. Blanchette) und Quickcheck (L. Bulwahn).

Macht all das automatisierte Zeug Isabelle zu einem automatisierten Theorembeweiser?

Letztendlich denke ich, dass die Unterscheidung zwischen "ATP" und "ITP" nur eine Art "Etikett" ist, das angibt, wie Sie Ihr System positionieren oder "verkaufen" möchten: ATPs behaupten, "Push-Button-Tools" zu sein, aber in In der Praxis müssen Sie (indirekt) interagieren, indem Sie Parameter oder Hinweise bereitstellen oder Ihr Problem neu formulieren. Das könnte aufgrund der langen Laufzeiten, die in der ATP-Community an der Tagesordnung sind, eine ziemliche Herausforderung sein.

Im Gegensatz dazu ist ein ITP-System für Personen gedacht, die vor Ort mit halbwegs angemessenem Zugriff auf interne Proofzustände warten, um zu sehen, was zum Fertigstellen eines Proofs fehlt. Ein ITP-System, das ATP-Tools nach Art von Isabelle zusammenfasst, könnte für mehr Benutzer und mehr Anwendungen attraktiver sein als ITP oder ATP allein.