Automatisierte Argumentation - Automated reasoning

In der Informatik , insbesondere in der Wissensrepräsentation und - folgerung und der Metalogik , widmet sich der Bereich des automatisierten Denkens dem Verständnis verschiedener Aspekte des Denkens . Das Studium des automatisierten Denkens hilft bei der Erstellung von Computerprogrammen, die es Computern ermöglichen, vollständig oder fast vollständig automatisch zu folgern. Obwohl das automatisierte Denken als Teilgebiet der künstlichen Intelligenz gilt , hat es auch Verbindungen zur theoretischen Informatik und Philosophie .

Die am weitesten entwickelten Teilbereiche des automatisierten Beweisens sind das automatisierte Theorembeweisen (und das weniger automatisierte, aber pragmatischere Teilgebiet des interaktiven Theorembeweisens ) und die automatisierte Beweisprüfung (angesehen als garantiert korrektes Denken unter festen Annahmen). Umfangreiche Arbeit wurde auch bei der Argumentation durch Analogie mit Induktion und Entführung geleistet .

Weitere wichtige Themen sind das Denken unter Unsicherheit und das nicht monotone Denken. Ein wichtiger Teil des Unsicherheitsfeldes ist der der Argumentation, wo zusätzlich zu der eher standardmäßigen automatisierten Deduktion weitere Beschränkungen der Minimalität und Konsistenz angewendet werden. Das OSCAR-System von John Pollock ist ein Beispiel für ein automatisiertes Argumentationssystem, das spezifischer ist als nur ein automatisierter Theorembeweiser.

Zu den Werkzeugen und Techniken des automatisierten Schließens gehören die klassische Logik und Kalküle, die Fuzzy-Logik , die Bayessche Inferenz , das Schließen mit maximaler Entropie und viele weniger formale Ad-hoc- Techniken.

Frühe Jahre

Die Entwicklung der formalen Logik spielte im Bereich des automatisierten Denkens eine große Rolle, was wiederum zur Entwicklung der künstlichen Intelligenz führte . Ein formaler Beweis ist ein Beweis, bei dem jede logische Schlussfolgerung auf die fundamentalen Axiome der Mathematik zurückgeprüft wurde. Alle logischen Zwischenschritte werden ausnahmslos mitgeliefert. An die Intuition wird nicht appelliert, auch wenn die Übersetzung von der Intuition in die Logik Routine ist. Somit ist ein formaler Beweis weniger intuitiv und weniger anfällig für logische Fehler.

Einige betrachten das Cornell Summer Meeting von 1957, an dem viele Logiker und Informatiker zusammenkamen, als Ursprung des automatisierten Denkens oder der automatisierten Deduktion . Andere sagen, dass es vorher mit dem Logic Theorist- Programm von Newell, Shaw und Simon von 1955 oder mit Martin Davis' Implementierung von Presburgers Entscheidungsverfahren von 1954 begann (das bewies, dass die Summe zweier gerader Zahlen gerade ist).

Automatisiertes Denken, obwohl ein bedeutendes und beliebtes Forschungsgebiet, erlebte in den achtziger und frühen neunziger Jahren einen „ KI-Winter “. Später wurde das Feld jedoch wiederbelebt. Zum Beispiel im Jahr 2005, Microsoft begann mit Verifikationstechnologie in vielen ihrer internen Projekten und plant eine logische Spezifikation und Prüfung Sprache in ihrer 2012 - Version von Visual C enthalten

Bedeutende Beiträge

Principia Mathematica war ein Meilensteinwerk der formalen Logik, das von Alfred North Whitehead und Bertrand Russell geschrieben wurde . Principia Mathematica - auch Prinzipien der Mathematik bedeutet - wurde mit dem Ziel geschrieben, alle oder einige der mathematischen Ausdrücke im Sinne einer symbolischen Logik abzuleiten. Principia Mathematica wurde 1910, 1912 und 1913 zunächst in drei Bänden veröffentlicht.

Logic Theorist (LT) war das erste Programm, das 1956 von Allen Newell , Cliff Shaw und Herbert A. Simon entwickelt wurde , um beim Beweisen von Theoremen "menschliches Denken nachzuahmen". -acht von ihnen. Zusätzlich zum Beweis der Sätze fand das Programm einen Beweis für einen der Sätze, der eleganter war als der von Whitehead und Russell. Nach einem erfolglosen Versuch, ihre Ergebnisse zu veröffentlichen, berichteten Newell, Shaw und Herbert 1958 in ihrer Veröffentlichung The Next Advance in Operation Research :

„Es gibt jetzt auf der Welt Maschinen, die denken, lernen und erschaffen. Darüber hinaus wird ihre Fähigkeit, diese Dinge zu tun, schnell zunehmen, bis (in einer sichtbaren Zukunft) die Bandbreite der Probleme, mit denen sie umgehen können, ähnlich groß sein wird der Bereich, auf den der menschliche Geist angewendet wurde."

Beispiele für formale Beweise

Jahr Satz Nachweissystem Formalisierer Traditioneller Beweis
1986 Erste Unvollständigkeit Boyer-Moore Shankar Gödel
1990 Quadratische Reziprozität Boyer-Moore Russinoff Eisenstein
1996 Grundlagen der Infinitesimalrechnung HOL-Licht Harrison Henstock
2000 Grundlagen- der Algebra Mizar Milewski Brynski
2000 Grundlagen- der Algebra Coq Geuverset al. Kneser
2004 Vier Farben Coq Gonthier Robertsonet al.
2004 Primzahl Isabelle Avigadet al. Selberg - Erdős
2005 Jordan-Kurve HOL-Licht Hales Thomassen
2005 Brouwer Fixpunkt HOL-Licht Harrison Kuhn
2006 Fliegenfleck 1 Isabelle Bauer- Nipkow Hales
2007 Cauchy-Rückstand HOL-Licht Harrison Klassik
2008 Primzahl HOL-Licht Harrison Analytischer Nachweis
2012 Feit-Thompson Coq Gonthier et al. Bender, Glauberman und Peterfalvi
2016 Boolesches Pythagoras verdreifacht Problem Formalisiert als SAT Heuleet al. Keiner

Nachweissysteme

Boyer-Moore-Theorembeweiser (NQTHM)
Das Design von NQTHM wurde von John McCarthy und Woody Bledsoe beeinflusst. 1971 in Edinburgh, Schottland, gestartet, war dies ein vollautomatischer Theorembeweiser, der mit Pure Lisp gebaut wurde . Die Hauptaspekte von NQTHM waren:
  1. die Verwendung von Lisp als Arbeitslogik.
  2. das Vertrauen auf ein Definitionsprinzip für totalrekursive Funktionen.
  3. die umfassende Verwendung von Umschreibungen und "symbolischer Bewertung".
  4. eine Induktionsheuristik, die auf dem Scheitern der symbolischen Auswertung beruht.
HOL-Licht
HOL Light wurde in OCaml geschrieben und bietet eine einfache und saubere logische Grundlage und eine übersichtliche Implementierung. Es ist im Wesentlichen ein weiterer Beweisassistent für die klassische Logik höherer Ordnung.
Coq
Coq wurde in Frankreich entwickelt und ist ein weiterer automatisierter Proof-Assistent, der automatisch ausführbare Programme aus Spezifikationen extrahieren kann, entweder als Objective CAML- oder Haskell- Quellcode. Eigenschaften, Programme und Beweise werden in der gleichen Sprache formalisiert, die als Kalkül der induktiven Konstruktionen (CIC) bezeichnet wird.

Anwendungen

Automatisiertes Denken wurde am häufigsten verwendet, um automatisierte Theorembeweiser zu erstellen. Oftmals benötigen Theorembeweiser jedoch eine menschliche Anleitung, um effektiv zu sein, und qualifizieren sich daher im Allgemeinen als Beweisassistenten . In einigen Fällen haben solche Beweiser neue Ansätze zum Beweis eines Theorems entwickelt. Der Logiktheoretiker ist ein gutes Beispiel dafür. Das Programm lieferte einen Beweis für einen der Sätze in Principia Mathematica , der effizienter war (weniger Schritte erforderte) als der Beweis von Whitehead und Russell. Automatisierte Argumentationsprogramme werden angewendet, um eine wachsende Zahl von Problemen in der formalen Logik, Mathematik und Informatik, Logikprogrammierung , Software- und Hardwareverifikation, Schaltungsdesign und vielen anderen zu lösen . Das TPTP (Sutcliffe und Suttner 1998) ist eine Bibliothek solcher Probleme, die regelmäßig aktualisiert wird. Außerdem findet regelmäßig ein Wettbewerb unter automatisierten Theorembeweisern auf der CADE- Konferenz statt (Pelletier, Sutcliffe und Suttner 2002); die Aufgaben für den Wettbewerb werden aus der TPTP-Bibliothek ausgewählt.

Siehe auch

Konferenzen und Workshops

Zeitschriften

Gemeinschaften

Verweise

  1. ^ Defourneaux, Gilles und Nicolas Peltier. " Analogie und Entführung bei der automatischen Deduktion ." IJCAI (1). 1997.
  2. ^ John L. Pollock
  3. ^ C. Hales, Thomas "Formaler Beweis" , University of Pittsburgh. Abgerufen am 19.10.2010
  4. ^ a b "Automated Deduction (AD)" , [Die Natur des PRL-Projekts] . Abgerufen am 19.10.2010
  5. ^ Martin Davis (1983). „Die Vor- und Frühgeschichte der automatisierten Deduktion“. In Jörg Siekmann; G. Wrightson (Hrsg.). Automation of Reasoning (1) – Klassische Arbeiten zur Computerlogik 1957–1966 . Heidelberg: Springer. S. 1–28. ISBN 978-3-642-81954-4. Hier: S.15
  6. ^ "Principia Mathematica" , an der Stanford University . Abgerufen 2010-10-19
  7. ^ „Der Logiktheoretiker und seine Kinder“ . Abgerufen 2010-10-18
  8. ^ Shankar, Natarajan Little Engines of Proof , Computer Science Laboratory, SRI International . Abgerufen 2010-10-19
  9. ^ Shankar, N. (1994), Metamathematik, Maschinen und Gödels Beweis , Cambridge, Großbritannien: Cambridge University Press, ISBN 9780521585330
  10. ^ Russinoff, David M. (1992), "Ein mechanischer Beweis der quadratischen Reziprozität", J. Autom. Grund. , 8 (1): 3–21, doi : 10.1007/BF00263446
  11. ^ Gonthier, G.; et al. (2013), "A Machine-Checked Proof of the Odd Order Theorem" (PDF) , in Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (Hrsg.), Interactive Theorem Proving , Lecture Notes in Computer Science, 7998 , S. 163–179, doi : 10.1007/978-3-642-39634-2_14 , ISBN 978-3-642-39633-5
  12. ^ Heule, Marijn JH ; Kullmann, Oliver; Marek, Victor W. (2016). „Lösen und Verifizieren des Booleschen Pythagoras-Triples-Problems durch Cube-and-Conquer“. Theorie und Anwendungen der Erfüllbarkeitsprüfung – SAT 2016 . Skript zur Vorlesung Informatik. 9710 . S. 228–245. arXiv : 1605.00723 . doi : 10.1007/978-3-319-40970-2_15 . ISBN 978-3-319-40969-6.
  13. ^ Der Boyer-Moore-Theorem-Beweiser . Abgerufen am 2010-10-23
  14. ^ Harrison, John HOL Light: eine Übersicht . Abgerufen 2010-10-23
  15. ^ Einführung in Coq . Abgerufen 2010-10-23
  16. ^ Automatisiertes Denken , Stanford Enzyklopädie . Abgerufen 2010-10-10

Externe Links