Nqthm - Nqthm

Nqthm er en setningsprover som noen ganger blir referert til som Boyer - Moore teoremprover . Det var en forløper til ACL2 .

Historie

Systemet ble utviklet av Robert S. Boyer og J Strother Moore , professorer i informatikk ved University of Texas, Austin . De begynte arbeidet med systemet i 1971 i Edinburgh , Skottland . Målet deres var å lage en helautomatisk, logikkbasert teoremprover. De brukte en variant av Pure LISP som arbeidslogikk.

Definisjoner

Definisjoner dannes som totalt rekursive funksjoner , systemet bruker omfattende omskriving og en induksjonsheuristikk som brukes når omskriving og noe de kalte symbolsk evaluering mislykkes.

Systemet ble bygget på toppen av Lisp og hadde noen veldig grunnleggende kunnskaper om det som ble kalt "Ground-zero", maskinens tilstand etter at den ble bootstrapped på en Common Lisp-implementering.

Dette er et eksempel på bevis på en enkel aritmetisk teorem. Funksjonen TIDER er en del av BOOT-STRAP (kalt en "satellitt") og er definert som 

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

Teorem formulering

Formuleringen av teoremet er også gitt i en Lisp-lignende syntaks: 

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

Skulle teoremet vise seg å være sant, vil det bli lagt til kunnskapsgrunnlaget for systemet og kan brukes som en omskrivningsregel for fremtidige bevis.

Selve beviset er gitt på en kvasi-naturlig språklig måte. Forfatterne velger tilfeldig typiske matematiske setninger for å legge inn trinnene i det matematiske beviset, noe som faktisk gjør bevisene ganske lesbare. Det er makroer for LaTeX som kan forvandle Lisp -strukturen til mer eller mindre lesbart matematisk språk.

Beviset på tiders kommutativitet fortsetter: 

 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))).

og etter å ha viklet seg gjennom en rekke induksjonsbevis, konkluderer det til slutt 

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

Bevis

Mange bevis er gjort eller bekreftet med systemet, spesielt

  • (1971) liste sammenkobling
  • (1973) innsettingssortering
  • (1974) en binær adder
  • (1976) en uttrykkskompilator for en stabelmaskin
  • (1978) særegenheten ved primfaktoriseringer
  • (1983) inverterbarhet av RSA -krypteringsalgoritmen
  • (1984) uløselighet av stoppeproblemet for Pure Lisp
  • (1985) FM8501 mikroprosessor (Warren Hunt)
  • (1986) Gödels ufullstendighetsteorem (Shankar)
  • (1988) CLI Stack (Bill Bevier, Warren Hunt, Matt Kaufmann, J Moore, Bill Young)
  • (1990) Gauss lov om kvadratisk gjensidighet (David Russinoff)
  • (1992) Bysantinske generaler og klokkesynkronisering (Bevier og Young)
  • (1992) En kompilator for en delmengde av Nqthm -språket (Arthur Flatau)
  • (1993) asynkron kommunikasjonsprotokoll med to faser
  • (1993) Motorola MC68020 og Berkeley C String Library (Yuan Yu)
  • (1994) Paris - Harrington Ramsey -setning ( Kenneth Kunen )
  • (1996) Ekvivalensen mellom NFSA og DFSA ( Debora Weber-Wulff )

PC-Nqthm

En kraftigere versjon, kalt PC-Nqthm (Proof-checker Nqthm) ble utviklet av Matt Kaufmann . Dette ga bevisverktøyene som systemet bruker automatisk til brukeren, slik at mer veiledning kan gis til beviset. Dette er en stor hjelp, ettersom systemet har en uproduktiv tendens til å vandre nedover uendelige kjeder av induktive bevis.

Litteratur

  • A Computational Logic Handbook, RS Boyer og J S. Moore, Academic Press (2. utgave), 1997.
  • The Boyer-Moore Theorem Prover and Its Interactive Enhancement, med M. Kaufmann og RS Boyer, Computers and Mathematics with Applications, 29 (2), 1995, s. 27–62.

Utmerkelser

Image
Prisen

I 2005 mottok Robert S. Boyer , Matt Kaufmann og J Strother Moore ACM Software System Award for sitt arbeid med Nqthm teorem prover.

Referanser

Eksterne linker