Automatisierte Theoremprüfung – Wikipedia

Posted on by
before-content-x4

Automatisierte Theoremprüfung (auch bekannt als ATP oder automatisierter Abzug) ist ein Teilgebiet des automatisierten Denkens und der mathematischen Logik, das sich mit dem Nachweis mathematischer Theoreme durch Computerprogramme befasst. Das automatisierte Denken über mathematische Beweise war ein wichtiger Impuls für die Entwicklung der Informatik.

Logische Grundlagen[edit]

Während die Wurzeln der formalisierten Logik auf Aristoteles zurückgehen, entwickelte sich am Ende des 19. und frühen 20. Jahrhunderts die moderne Logik und die formalisierte Mathematik. Frege’s Begriffsschrift (1879) führten sowohl eine vollständige Aussagenrechnung als auch eine im Wesentlichen moderne Prädikatenlogik ein.[1] Seine Grundlagen der Arithmetik, veröffentlicht 1884,[2] ausgedrückt (Teile der) Mathematik in formaler Logik. Dieser Ansatz wurde von Russell und Whitehead in ihrem Einfluss fortgesetzt Principia Mathematica, erstmals veröffentlicht 1910–1913,[3] und mit einer überarbeiteten zweiten Ausgabe im Jahr 1927.[4] Russell und Whitehead dachten, sie könnten alle mathematischen Wahrheiten unter Verwendung von Axiomen und Inferenzregeln der formalen Logik ableiten, was den Prozess im Prinzip für die Automatisierung öffnet. 1920 vereinfachte Thoralf Skolem ein früheres Ergebnis von Leopold Löwenheim, was zum Löwenheim-Skolem-Theorem und 1930 zur Vorstellung eines Herbrand-Universums und einer Herbrand-Interpretation führte, die die (Un-) Erfüllbarkeit von Formeln erster Ordnung (und damit) ermöglichten die Gültigkeit eines Theorems) auf (möglicherweise unendlich viele) Probleme der Erfüllbarkeit von Aussagen zu reduzieren.[5]

1929 zeigte Mojżesz Presburger, dass die Theorie der natürlichen Zahlen mit Addition und Gleichheit (jetzt zu seinen Ehren Presburger-Arithmetik genannt) entscheidbar ist, und gab einen Algorithmus an, mit dem festgestellt werden konnte, ob ein bestimmter Satz in der Sprache wahr oder falsch war.[6][7]

Kurz nach diesem positiven Ergebnis veröffentlichte Kurt Gödel jedoch Über formal unentscheidbare Sätze von Principia Mathematica und verwandten Systemen (1931), was zeigt, dass es in jedem ausreichend starken axiomatischen System wahre Aussagen gibt, die im System nicht bewiesen werden können. Dieses Thema wurde in den 1930er Jahren von Alonzo Church und Alan Turing weiterentwickelt, die einerseits zwei unabhängige, aber äquivalente Definitionen der Berechenbarkeit gaben und andererseits konkrete Beispiele für unentscheidbare Fragen gaben.

Erste Implementierungen[edit]

Kurz nach dem Zweiten Weltkrieg wurden die ersten Universalcomputer verfügbar. 1954 programmierte Martin Davis den Presburger-Algorithmus für einen JOHNNIAC-Vakuumröhrencomputer am Princeton Institute for Advanced Study. Laut Davis “bestand sein großer Triumph darin, zu beweisen, dass die Summe von zwei geraden Zahlen gerade ist”.[7][8] Ehrgeiziger war die Logic Theory Machine von 1956, ein Abzugssystem für die Aussagenlogik der Principia Mathematica, entwickelt von Allen Newell, Herbert A. Simon und JC Shaw.[9] Die Logic Theory Machine lief ebenfalls auf einem JOHNNIAC und konstruierte Beweise aus einem kleinen Satz von Satzaxiomen und drei Ableitungsregeln: Modus Ponens, (Satz-) Variablensubstitution und das Ersetzen von Formeln durch ihre Definition. Das System verwendete heuristische Anleitungen und konnte 38 der ersten 52 Sätze der Principia.[7]

Der “heuristische” Ansatz der Logic Theory Machine versuchte, menschliche Mathematiker zu emulieren, und konnte nicht garantieren, dass auch im Prinzip für jeden gültigen Satz ein Beweis gefunden werden konnte. Im Gegensatz dazu erreichten andere systematischere Algorithmen zumindest theoretisch die Vollständigkeit der Logik erster Ordnung. Anfängliche Ansätze stützten sich auf die Ergebnisse von Herbrand und Skolem, um eine Formel erster Ordnung in sukzessive größere Sätze von Satzformeln umzuwandeln, indem Variablen mit Begriffen aus dem Herbrand-Universum instanziiert wurden. Die Satzformeln könnten dann unter Verwendung einer Reihe von Methoden auf Unzufriedenheit überprüft werden. Gilmores Programm verwendete die Umwandlung in eine disjunktive Normalform, eine Form, in der die Erfüllbarkeit einer Formel offensichtlich ist.[7][10]

Entscheidbarkeit des Problems[edit]

Abhängig von der zugrunde liegenden Logik variiert das Problem der Entscheidung über die Gültigkeit einer Formel von trivial bis unmöglich. Für den häufigen Fall der Aussagenlogik ist das Problem entscheidbar, aber co-NP-vollständig, und daher wird angenommen, dass für allgemeine Beweisaufgaben nur Exponentialzeitalgorithmen existieren. Für einen Prädikatenkalkül erster Ordnung besagt der Vollständigkeitssatz von Gödel, dass die Sätze (nachweisbare Aussagen) genau die logisch gültigen wohlgeformten Formeln sind, sodass die Identifizierung gültiger Formeln rekursiv aufzählbar ist: Bei unbegrenzten Ressourcen kann schließlich jede gültige Formel bewiesen werden. Jedoch, ungültig Formeln (diejenigen, die sind nicht eine bestimmte Theorie) kann nicht immer erkannt werden.

Das Obige gilt für Theorien erster Ordnung wie die Peano-Arithmetik. Für ein bestimmtes Modell, das durch eine Theorie erster Ordnung beschrieben werden kann, können einige Aussagen in der zur Beschreibung des Modells verwendeten Theorie wahr, aber unentscheidbar sein. Zum Beispiel wissen wir durch Gödels Unvollständigkeitssatz, dass jede Theorie, deren richtige Axiome für die natürlichen Zahlen gelten, nicht alle Aussagen erster Ordnung für die natürlichen Zahlen beweisen kann, selbst wenn die Liste der richtigen Axiome unendlich aufzählbar sein darf. Daraus folgt, dass ein automatisierter Theorembeweiser bei der Suche nach einem Beweis nicht genau dann beendet werden kann, wenn die untersuchte Aussage in der verwendeten Theorie unentscheidbar ist, selbst wenn sie im interessierenden Modell zutrifft. Trotz dieser theoretischen Grenze können Theoremprüfer in der Praxis viele schwierige Probleme lösen, selbst in Modellen, die von keiner Theorie erster Ordnung (wie den ganzen Zahlen) vollständig beschrieben werden.

Verwandte Probleme[edit]

Ein einfacheres, aber verwandtes Problem ist Beweisüberprüfung, wenn ein vorhandener Beweis für einen Satz als gültig bestätigt wird. Hierzu ist es im Allgemeinen erforderlich, dass jeder einzelne Beweisschritt durch eine primitive rekursive Funktion oder ein Programm überprüft werden kann, und daher ist das Problem immer entscheidbar.

Da die von automatisierten Theoremprüfern erzeugten Beweise typischerweise sehr groß sind, ist das Problem der Beweiskomprimierung entscheidend, und es wurden verschiedene Techniken entwickelt, die darauf abzielen, die Ausgabe des Prüfers kleiner und folglich leichter verständlich und überprüfbar zu machen.

Beweisassistenten verlangen von einem menschlichen Benutzer, dass er dem System Hinweise gibt. Abhängig vom Automatisierungsgrad kann der Prüfer im Wesentlichen auf einen Proof-Prüfer reduziert werden, wobei der Benutzer den Proof auf formale Weise bereitstellt, oder wichtige Proof-Aufgaben können automatisch ausgeführt werden. Interaktive Prüfer werden für eine Vielzahl von Aufgaben verwendet, aber selbst vollautomatische Systeme haben eine Reihe interessanter und schwieriger Theoreme bewiesen, darunter mindestens eines, das sich menschlichen Mathematikern seit langem entzogen hat, nämlich die Robbins-Vermutung.[11][12] Diese Erfolge sind jedoch sporadisch und die Arbeit an schwierigen Problemen erfordert normalerweise einen kompetenten Benutzer.

Manchmal wird eine andere Unterscheidung zwischen Theorembeweis und anderen Techniken getroffen, bei denen ein Prozess als Theorembeweis betrachtet wird, wenn er aus einem traditionellen Beweis besteht, der mit Axiomen beginnt und neue Inferenzschritte unter Verwendung von Inferenzregeln erzeugt. Andere Techniken würden die Modellprüfung umfassen, die im einfachsten Fall die Brute-Force-Aufzählung vieler möglicher Zustände beinhaltet (obwohl die tatsächliche Implementierung von Modellprüfern viel Klugheit erfordert und sich nicht einfach auf Brute-Force reduziert).

Es gibt hybride Theoremprüfsysteme, die die Modellprüfung als Inferenzregel verwenden. Es gibt auch Programme, die geschrieben wurden, um einen bestimmten Satz zu beweisen, mit einem (normalerweise informellen) Beweis, dass der Satz wahr ist, wenn das Programm mit einem bestimmten Ergebnis endet. Ein gutes Beispiel hierfür war der maschinengestützte Beweis des Vierfarbensatzes, der als erster behaupteter mathematischer Beweis, der vom Menschen aufgrund der enormen Größe der Programmberechnung im Wesentlichen nicht verifiziert werden konnte, sehr kontrovers war (solche Beweise werden als nicht bezeichnet) -befragbare Beweise). Ein weiteres Beispiel für einen programmgestützten Beweis ist der, der zeigt, dass das Spiel Connect Four immer vom ersten Spieler gewonnen werden kann.

Industrielle Anwendungen[edit]

Die kommerzielle Verwendung der automatisierten Theoremprüfung konzentriert sich hauptsächlich auf das Design und die Verifizierung integrierter Schaltkreise. Seit dem Pentium FDIV-Fehler wurden die komplizierten Gleitkommaeinheiten moderner Mikroprozessoren mit besonderer Sorgfalt entwickelt. AMD, Intel und andere verwenden automatisierte Theoreme, um zu überprüfen, ob Divisions- und andere Operationen in ihren Prozessoren korrekt implementiert sind.

Theorem erster Ordnung beweisen[edit]

In den späten 1960er Jahren begannen Agenturen, die Forschung im Bereich des automatisierten Abzugs finanzierten, die Notwendigkeit praktischer Anwendungen zu betonen. Einer der ersten fruchtbaren Bereiche war die Programmüberprüfung, bei der Theoremprüfer erster Ordnung auf das Problem der Überprüfung der Richtigkeit von Computerprogrammen in Sprachen wie Pascal, Ada usw. angewendet wurden. Unter den frühen Programmüberprüfungssystemen war der Stanford Pascal Verifier bemerkenswert entwickelt von David Luckham an der Stanford University. Dies basierte auf dem Stanford Resolution Prover, der ebenfalls in Stanford nach dem Auflösungsprinzip von John Alan Robinson entwickelt wurde. Dies war das erste automatisierte Abzugssystem, das die Fähigkeit demonstrierte, mathematische Probleme zu lösen, die in den Mitteilungen der American Mathematical Society angekündigt wurden, bevor Lösungen offiziell veröffentlicht wurden.[citation needed]

Theoremprüfung erster Ordnung ist eines der ausgereiftesten Teilgebiete der automatisierten Theoremprüfung. Die Logik ist ausdrucksstark genug, um die Spezifikation beliebiger Probleme zu ermöglichen, oft auf einigermaßen natürliche und intuitive Weise. Auf der anderen Seite ist es immer noch halb entscheidbar, und es wurden eine Reihe von soliden und vollständigen Kalkülen entwickelt, die dies ermöglichen völlig automatisierte Systeme.[citation needed] Ausdrucksstärkere Logiken wie Logiken höherer Ordnung ermöglichen die bequeme Darstellung eines größeren Spektrums von Problemen als Logik erster Ordnung, aber der Satz, der diese Logiken beweist, ist weniger gut entwickelt.[13][14]

Benchmarks, Wettbewerbe und Quellen[edit]

Die Qualität der implementierten Systeme hat von der Existenz einer großen Bibliothek mit Standard-Benchmark-Beispielen profitiert – der TPTP-Problembibliothek (Thousands of Problems for Theorem Provers)[15] – sowie aus dem CADE ATP System Competition (CASC), einem jährlichen Wettbewerb von Systemen erster Ordnung für viele wichtige Klassen von Problemen erster Ordnung.

Einige wichtige Systeme (alle haben mindestens eine CASC-Wettbewerbsabteilung gewonnen) sind nachstehend aufgeführt.

Das Theorem Prover Museum ist eine Initiative, um die Quellen von Theorembeweisungssystemen für zukünftige Analysen zu erhalten, da sie wichtige kulturhistorische Artefakte sind. Es hat die Quellen vieler der oben genannten Systeme.

Beliebte Techniken[edit]

Softwaresysteme[edit]

Vergleich
Name Lizenz-Typ Internetservice Bibliothek Eigenständige Letztes Update (JJJJ-MM-TT-Format)
ACL2 3-Klausel BSD Nein Nein Ja Mai 2019
Prover9 / Otter Public Domain Über das System auf TPTP Ja Nein 2009
Scherz GPLv2 Ja Ja Nein 15. Mai 2015
PVS GPLv2 Nein Ja Nein 14. Januar 2013
Leo II BSD-Lizenz Über das System auf TPTP Ja Ja 2013
EQP ? Nein Ja Nein Mai 2009
TRAURIG GPLv3 Ja Ja Nein 27. August 2008
PhoX ? Nein Ja Nein 28. September 2017
KeYmaera GPL Über Java Webstart Ja Ja 11. März 2015
Gandalf ? Nein Ja Nein 2009
E. GPL Über das System auf TPTP Nein Ja 4. Juli 2017
SNARK Mozilla Public License 1.1 Nein Ja Nein 2012
Vampir Vampir-Lizenz Über das System auf TPTP Ja Ja 14. Dezember 2017
Theorem Proving System (TPS) TPS-Vertriebsvereinbarung Nein Ja Nein 4. Februar 2012
SPASS FreeBSD-Lizenz Ja Ja Ja November 2005
IsaPlanner GPL Nein Ja Ja 2007
Schlüssel GPL Ja Ja Ja 11. Oktober 2017
Prinzessin lgpl v2.1 Über Java Webstart und System auf TPTP Ja Ja 27. Januar 2018
iProver GPL Über das System auf TPTP Nein Ja 2018
Meta-Theorem Freeware Nein Nein Ja April 2020
Z3 Theorembeweiser MIT-Lizenz Ja Ja Ja 19. November 2019

Gratis Software[edit]

Proprietäre Software[edit]

Siehe auch[edit]

  1. ^ Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert.
  2. ^ Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Archiviert von das Original (PDF) am 26.09.2007. Abgerufen 2012-09-02.
  3. ^ Bertrand Russell; Alfred North Whitehead (1910–1913). Principia Mathematica (1. Aufl.). Cambridge University Press.
  4. ^ Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica (2. Aufl.). Cambridge University Press.
  5. ^ Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration.
  6. ^ Presburger, Mojżesz (1929). “Über die Vollständigkeit eines anderen Systems der Arithmetik ganzer Zahlen, in der neuen als auch Operation hervortritt”. Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101.
  7. ^ ein b c d Davis, Martin (2001), “Die frühe Geschichte des automatisierten Abzugs”in Robinson Alan; Voronkov, Andrei (Hrsg.), Handbuch des automatisierten Denkens, 1Elsevier)
  8. ^ Bibel, Wolfgang (2007). “Frühgeschichte und Perspektiven des automatisierten Abzugs” (PDF). Ki 2007. LNAI. Springer (4667): 2–18. Abgerufen 2. September 2012.
  9. ^ Wolfram, Stephen (2002). Eine neue Art von Wissenschaft. Wolfram Media, Inc. p. 1157. ISBN 1-57955-008-8.
  10. ^ Gilmore, Paul (1960). “Ein Beweisverfahren für die Quantifizierungstheorie: ihre Rechtfertigung und Verwirklichung”. IBM Journal für Forschung und Entwicklung. 4: 28–35. doi:10.1147 / rd.41.0028.
  11. ^ WW McCune (1997). “Lösung des Robbins-Problems”. Journal of Automated Reasoning. 19 (3): 263–276. doi:10.1023 / A: 1005843212881.
  12. ^ Gina Kolata (10. Dezember 1996). “Computer Math Proof zeigt Argumentationskraft”. Die New York Times. Abgerufen 2008-10-11.
  13. ^ Kerber, Manfred. “”Wie man Sätze höherer Ordnung in der Logik erster Ordnung beweist(1999).
  14. ^ Benzmüller, Christoph et al. “”LEO-II-ein kooperativer automatischer Theorembeweiser für die klassische Logik höherer Ordnung (Systembeschreibung)“Internationale gemeinsame Konferenz über automatisiertes Denken. Springer, Berlin, Heidelberg, 2008.
  15. ^ Sutcliffe, Geoff. “Die TPTP-Problembibliothek für die automatisierte Theoremprüfung”. Abgerufen 15. Juli 2019.
  16. ^ Bundy, Alan. Die Automatisierung von Beweisen durch mathematische Induktion. 1999.
  17. ^ Artosi, Alberto, Paola Cattabriga und Guido Governatori. “”Ked: Ein Beweis für einen deontischen SatzElfte Internationale Konferenz über Logikprogrammierung (ICLP’94). 1994.
  18. ^ Otten, Jens; Bibel, Wolfgang (2003). “LeanCoP: Lean Connection-basiertes Theorem beweisen”. Zeitschrift für symbolische Berechnung. 36 (1–2): 139–161. doi:10.1016 / S0747-7171 (03) 00037-3.
  19. ^ del Cerro, Luis Farinas et al. “”Lotrec: der generische Tableau-Prover für Modal- und Beschreibungslogiken“Internationale gemeinsame Konferenz über automatisiertes Denken. Springer, Berlin, Heidelberg, 2001.
  20. ^ Hickey, Jason et al. “”MetaPRL – eine modulare logische Umgebung. “Internationale Konferenz über Theorembeweise in der Logik höherer Ordnung. Springer, Berlin, Heidelberg, 2003.
  21. ^ [1] Mathematica-Dokumentation

Verweise[edit]

  • Chin-Liang Chang; Richard Char-Tung Lee (1973). Beweis der symbolischen Logik und des mechanischen Theorems. Akademische Presse.
  • Loveland, Donald W. (1978). Automatisierte Theoremprüfung: Eine logische Basis. Grundlagen der Informatik Band 6. Nordholland Publishing.
  • Luckham, David (1990). Programmieren mit Spezifikationen: Eine Einführung in Anna, eine Sprache zum Spezifizieren von Ada-Programmen. Springer-Verlag Texte und Monographien der Informatik, 421 S. ISBN 978-1461396871.

Externe Links[edit]

after-content-x4