Nkthm - Nqthm

Nqthm jest dowodzicielem twierdzenia czasami określanym jako dowodzący twierdzenia Boyera-Moore'a . Był prekursorem ACL2 .

Historia

System został opracowany przez Roberta S. Boyera i J Strothera Moore'a , profesorów informatyki z University of Texas w Austin . Zaczęli pracę w systemie w 1971 roku w Edynburgu , w Szkocji . Ich celem było stworzenie w pełni automatycznego, opartego na logice dowodzenia twierdzenia. Użyli wariantu Pure LISP jako logiki działania.

Definicje

Definicje są tworzone jako funkcje całkowicie rekurencyjne , system intensywnie wykorzystuje przepisywanie i heurystykę indukcyjną, która jest używana podczas przepisywania, i coś, co nazwali oceną symboliczną, zawodzi.

System został zbudowany na Lispie i miał bardzo podstawową wiedzę na temat tego, co nazywano "Ground-zero", stanem maszyny po załadowaniu jej do implementacji Common Lisp.

To jest przykład dowodu prostego twierdzenia arytmetycznego. Funkcja TIMES jest częścią BOOT-STRAP (zwaną „satelitą”) i jest zdefiniowana jako 

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

Sformułowanie twierdzenia

Sformułowanie twierdzenia jest również podane w składni podobnej do Lispa: 

 (prove-lemma commutativity-of-times (rewrite)
   (equal (times x z) (times z x)))

Jeśli twierdzenie okaże się prawdziwe, zostanie dodane do bazy wiedzy systemu i może być użyte jako reguła przepisywania dla przyszłych dowodów.

Sam dowód jest podany w języku quasi-naturalnym. Autorzy losowo wybierają typowe wyrażenia matematyczne do osadzenia kroków w dowodzie matematycznym, co w rzeczywistości sprawia, że ​​dowody są całkiem czytelne. Istnieją makra dla LaTeX-a, które mogą przekształcić strukturę Lisp na mniej lub bardziej czytelny język matematyczny.

Dowód przemienności czasów trwa dalej: 

 Give the conjecture the name *1.
 We will appeal to induction.  Two inductions are suggested by terms in the conjecture, 
 both of which are flawed.  We limit our consideration to the two suggested by the 
 largest number of nonprimitive recursive functions in the conjecture.  Since both of 
 these are equally likely, we will choose arbitrarily.  We will induct according to 
 the following scheme:
       (AND (IMPLIES (ZEROP X) (p X Z))
          (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z))
                   (p X Z))).
 Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
 us that the measure (COUNT X) decreases according to the well-founded relation
 LESSP in each induction step of the scheme.  The above induction scheme
 produces the following two new conjectures:
 Case 2. (IMPLIES (ZEROP X)
                  (EQUAL (TIMES X Z) (TIMES Z X))).

i po nawinięciu się przez szereg dowodów indukcyjnych, w końcu dochodzi do wniosku, że 

Case 1. (IMPLIES (AND (NOT (ZEROP Z))
                      (EQUAL 0 (TIMES (SUB1 Z) 0)))
                 (EQUAL 0 (TIMES Z 0))).
This simplifies, expanding the definitions of ZEROP, TIMES, PLUS, and EQUAL, to:
     T.
That finishes the proof of *1.1, which also finishes the proof of *1.
Q.E.D.
[ 0.0 1.2 0.5 ]
COMMUTATIVITY-OF-TIMES

Dowody

Wiele dowodów zostało wykonanych lub potwierdzonych w systemie, w szczególności:

  • (1971) konkatenacja list
  • (1973) sortowanie wstawiania
  • (1974) sumator binarny
  • (1976) kompilator wyrażeń dla maszyny stosowej
  • (1978) unikatowość faktoryzacji pierwszych
  • (1983) odwracalność algorytmu szyfrowania RSA
  • (1984) nierozwiązywalność problemu zatrzymania dla Pure Lisp
  • (1985) mikroprocesor FM8501 (Warren Hunt)
  • (1986) Twierdzenie o niezupełności Gödla (Shankar)
  • (1988) CLI Stack (Bill Bevier, Warren Hunt, Matt Kaufmann, J Moore, Bill Young)
  • (1990) Prawo Gaussa o kwadratowej wzajemności (David Russinoff)
  • (1992) Generałowie bizantyjscy i synchronizacja zegara (Bevier i Young)
  • (1992) Kompilator podzbioru języka Nqthm (Arthur Flatau)
  • (1993) dwufazowy znak asynchroniczny protokół komunikacyjny
  • (1993) Motorola MC68020 i Berkeley C String Library (Yuan Yu)
  • (1994) Twierdzenie Parisa-Harringtona Ramseya ( Kenneth Kunen )
  • (1996) Równoważność NFSA i DFSA ( Debora Weber-Wulff )

PC-Nqthm

Bardziej wydajna wersja, nazwana PC-Nqthm (Proof-checker Nqthm) została opracowana przez Matta Kaufmanna . Dało to użytkownikowi narzędzia sprawdzające, które system wykorzystuje automatycznie, dzięki czemu można uzyskać więcej wskazówek dotyczących dowodu. Jest to bardzo pomocne, ponieważ system ma nieproduktywną tendencję do wędrowania w dół nieskończonych łańcuchów dowodów indukcyjnych.

Literatura

  • Podręcznik logiki obliczeniowej, RS Boyer i J S. Moore, Academic Press (wydanie drugie), 1997.
  • The Boyer-Moore Theorem Prover and its Interactive Enhancement, z M. Kaufmann i RS Boyer, Computers and Mathematics with Applications, 29(2), 1995, s. 27-62.

Nagrody

Nagroda

W 2005 roku Robert S. Boyer , Matt Kaufmann i J Strother Moore otrzymali nagrodę ACM Software System Award za pracę nad dowodzeniem twierdzenia Nqthm.

Bibliografia

Zewnętrzne linki