Nqthm - Nqthm

Nqthm er en sætningsprover, der undertiden omtales som Boyer -Moore sætningsprover . Det var en forløber for ACL2 .

Historie

Systemet blev udviklet af Robert S. Boyer og J Strother Moore , professorer i datalogi ved University of Texas, Austin . De begyndte at arbejde på systemet i 1971 i Edinburgh , Skotland . Deres mål var at lave en fuldautomatisk, logikbaseret sætningsprover. De brugte en variant af Pure LISP som arbejdslogik.

Definitioner

Definitioner dannes som totalt rekursive funktioner , systemet gør omfattende brug af omskrivning og en induktionsheuristik , der bruges ved omskrivning og noget, som de kaldte symbolsk evaluering mislykkes.

Systemet blev bygget oven på Lisp og havde en meget grundlæggende viden om, hvad der blev kaldt "Ground-zero", maskinens tilstand efter at have bootstrapped det på en Common Lisp-implementering.

Dette er et eksempel på beviset på en simpel aritmetisk sætning. Funktionen TIMES er en del af BOOT-STRAP (kaldet en "satellit") og er defineret til at være 

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

Sætningsformulering

Formuleringen af ​​sætningen er også givet i en Lisp-lignende syntaks: 

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

Skulle teoremet vise sig at være sandt, tilføjes det til systemets vidensgrundlag og kan bruges som en omskrivningsregel for fremtidige beviser.

Selve beviset er givet på en næsten naturlig sproglig måde. Forfatterne vælger tilfældigt typiske matematiske sætninger til at indlejre trinene i det matematiske bevis, hvilket faktisk gør beviserne ret læsbare. Der er makroer til LaTeX, der kan omdanne Lisp -strukturen til et mere eller mindre læseligt matematisk sprog.

Beviset for tidernes kommutativitet fortsætter: 

 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 efter at have viklet sig igennem en række induktionsbeviser, konkluderer det endelig 

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

Beviser

Mange beviser er blevet udført eller bekræftet med systemet, især

  • (1971) liste sammenkædning
  • (1973) indsættelsessort
  • (1974) en binær adder
  • (1976) en udtrykskompilator til en stakemaskine
  • (1978) unikt ved primære faktoriseringer
  • (1983) inversibilitet af RSA -krypteringsalgoritmen
  • (1984) uløselighed af stopproblemet for Pure Lisp
  • (1985) FM8501 mikroprocessor (Warren Hunt)
  • (1986) Gödel's ufuldstændighedssætning (Shankar)
  • (1988) CLI Stack (Bill Bevier, Warren Hunt, Matt Kaufmann, J Moore, Bill Young)
  • (1990) Gauss 'lov om kvadratisk gensidighed (David Russinoff)
  • (1992) Byzantinske generaler og ur -synkronisering (Bevier og Young)
  • (1992) En kompilator til en delmængde af Nqthm -sproget (Arthur Flatau)
  • (1993) asynkron kommunikationsprotokol med to faser
  • (1993) Motorola MC68020 og Berkeley C String Library (Yuan Yu)
  • (1994) Paris – Harrington Ramsey -sætning ( Kenneth Kunen )
  • (1996) NFSA og DFSA's ækvivalens ( Debora Weber-Wulff )

PC-Nqthm

En mere kraftfuld version, kaldet PC-Nqthm (Proof-checker Nqthm) blev udviklet af Matt Kaufmann . Dette gav de bevisværktøjer, som systemet bruger automatisk til brugeren, så der kan gives mere vejledning til beviset. Dette er en stor hjælp, da systemet har en uproduktiv tendens til at vandre ned ad uendelige kæder af induktive beviser.

Litteratur

  • A Computational Logic Handbook, RS Boyer og J S. Moore, Academic Press (2. udgave), 1997.
  • 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.

Priser

Image
Prisen

I 2005 modtog Robert S. Boyer , Matt Kaufmann og J Strother Moore ACM Software System Award for deres arbejde med Nqthm -sætningsproveren.

Referencer

eksterne links