Nqthm

Nqthm ist ein Theorembeweiser, der manchmal auch als Boyer-Moore-Theorembeweiser bezeichnet wird . Er war ein Vorläufer von ACL2 . ^{[ 1 ]}

Das System wurde von Robert S. Boyer und J. Strother Moore , Professoren für Informatik an der University of Texas in Austin, entwickelt . Sie begannen 1971 in Edinburgh , Schottland , mit der Arbeit daran . Ihr Ziel war ein vollautomatischer, logikbasierter Theorembeweiser. Als Arbeitslogik verwendeten sie eine Variante von Pure LISP .

Die Definitionen werden als vollständig rekursive Funktionen gebildet , das System nutzt ausgiebig das Umschreiben und eine Induktionsheuristik , die beim Umschreiben verwendet wird, und etwas, das sie symbolische Auswertung nennen, schlägt fehl.

Das System basierte auf Lisp und verfügte über sehr grundlegende Kenntnisse in dem, was als „Ground-Zero“ bezeichnet wurde, dem Zustand der Maschine nach dem Bootstrapping auf einer Common Lisp-Implementierung.

Dies ist ein Beispiel für den Beweis eines einfachen arithmetischen Satzes. Die Funktion TIMES ist Teil des BOOT-STRAP (auch „Satellit“ genannt) und ist wie folgt definiert:

( DEFN TIMES ( X Y ) ( IF ( ZEROP X ) 0 ( PLUS Y ( TIMES ( SUB1 X ) Y ))))

Die Formulierung des Theorems ist ebenfalls in einer Lisp-ähnlichen Syntax angegeben:

( Beweis-Lemma Kommutativität der Zeiten ( Umschreiben ) ( gleich ( mal x z ) ( mal z x )))

Sollte sich der Satz als wahr erweisen, wird er in die Wissensbasis des Systems aufgenommen und kann als Umformulierungsregel für zukünftige Beweise verwendet werden.

Der Beweis selbst ist in einer Art quasi-natürlicher Sprache verfasst. Die Autoren wählen willkürlich typische mathematische Formulierungen, um die einzelnen Schritte des Beweises einzubetten, was die Beweise tatsächlich recht lesbar macht. Es gibt Makros für LaTeX , die die Lisp-Struktur in eine mehr oder weniger lesbare mathematische Sprache umwandeln können.

Der Beweis der Kommutativität der Zeiten wird fortgesetzt:

Die Vermutung erhält den Namen *1. Wir werden uns auf die Induktion berufen. Zwei Induktionswege werden durch Ausdrücke in der Vermutung nahegelegt. Beide Ansätze sind fehlerhaft. Wir beschränken unsere Betrachtung auf die beiden vom Autor vorgeschlagenen Ansätze. größte Anzahl nichtprimitiver rekursiver Funktionen in der Vermutung. Da beide von Diese sind gleich wahrscheinlich, wir wählen willkürlich. Wir induzieren gemäß das folgende Schema: (UND (IMPLIZIERT (NULL X) (p XZ)) (IMPLIES (AND (NOT (NEROP X)) (p (SUB1 X) Z)) (p XZ))). Lineare Arithmetik, das Lemma COUNT-NUMBERP und die Definition von ZEROP informieren Wir wissen, dass die Kennzahl (COUNT X) gemäß der wohlbegründeten Beziehung abnimmt. LESSP in jedem Induktionsschritt des Schemas. Das obige Induktionsschema führt zu den folgenden zwei neuen Vermutungen: Fall 2. (IMPLIES (NULL X)) (GLEICH (MAL XZ) (MAL ZX))). 

und nachdem es sich durch eine Reihe von Induktionsbeweisen gequält hat, kommt es schließlich zu dem Schluss, dass

Fall 1. (IMPLIES (UND (NICHT (NULL Z))) (GLEICH 0 (MAL (SUB1 Z) 0))) (GLEICH 0 (MAL Z 0))). Dies vereinfacht die Definitionen von NULL, ZEITPUNKT, PLUS und GLEICH und erweitert sie zu: T. Damit ist der Beweis von *1.1 abgeschlossen, wodurch auch der Beweis von *1 abgeschlossen ist. QED [ 0,0 1,2 0,5 ] KOMMUTATIVITÄT DER ZEITEN 

Viele Nachweise wurden mit dem System erbracht oder bestätigt, insbesondere

• (1971) Listenverkettung
• (1973) Einfügungssortierung
• (1974) ein Binäraddierer
• (1976) ein Ausdruckscompiler für eine Stackmaschine
• (1978) Eindeutigkeit der Primfaktorzerlegungen
• (1983) Invertierbarkeit des RSA-Verschlüsselungsalgorithmus
• (1984) Unlösbarkeit des Halteproblems für reines Lisp
• (1985) FM8501 Mikroprozessor (Warren Hunt) ^{[ 2 ]}
• (1986) Gödels Unvollständigkeitssatz (Shankar)
• (1988) CLI Stack (Bill Bevier, Warren Hunt, Matt Kaufmann, J Moore, Bill Young)
• (1990) Gaußsches Gesetz der quadratischen Reziprozität (David Russinoff)
• (1992) Byzantinische Generäle und die Uhrsynchronisation (Bevier und Young)
• (1992) Ein Compiler für eine Teilmenge der Nqthm-Sprache (Arthur Flatau)
• (1993) Bi-Phase Mark Asynchronous Communications Protocol
• (1993) Motorola MC68020 und Berkeley C String Library (Yuan Yu)
• (1994) Satz von Paris–Harrington Ramsey ( Kenneth Kunen )
• (1996) Die Äquivalenz von NFSA und DFSA ( Debora Weber-Wulff )

Eine leistungsfähigere Version namens PC-Nqthm (Proof-checker Nqthm) wurde von Matt Kaufmann entwickelt . Diese stellt dem Benutzer die vom System automatisch verwendeten Beweiswerkzeuge zur Verfügung, sodass der Beweisprozess gezielter gesteuert werden kann. Dies ist eine große Hilfe, da das System dazu neigt, sich in endlosen Ketten induktiver Beweise zu verlieren.

• Boyer, Robert S .; Moore, J. Strother (1998). A Computational Logic Handbook (2. Aufl.). San Diego : Academic Press . ISBN 9780121229559OCLC  38515159 .​
• Boyer, RS ; Kaufmann, M ; Moore, JS (Januar 1995). „Der Boyer-Moore-Theorembeweiser und seine interaktive Erweiterung“ . Computers & Mathematics with Applications . 29 (2): 27–62 . Abgerufen am 29. Mai 2025 .

Im Jahr 2005 erhielten Robert S. Boyer , Matt Kaufmann und J. Strother Moore den ACM Software System Award für ihre Arbeit am Nqthm-Theorembeweiser. ^{[ 3 ]}

• Das automatisierte Schlussfolgerungssystem, Nqthm
• Der Boyer-Moore-Theorembeweiser (NQTHM)
• Auch wenn das System nicht mehr unterstützt wird, ist es weiterhin unter [1] verfügbar.
• Ausführbare Version auf GitHub : [2]