Rechnergestuetztes Beweisen

Hofmann, 2008-01-23

Entscheidungsprozeduren in Coq
==============================

Integration Entsch.proz. in Theorembeweiser

unsicher:  einfach dazubauen (PVS)

sicher: 1. Als Taktik ausprogrammieren (LCF)
        2. Externe Zertifikate
        3. Reflektion (Bsp: 4-Farben-Satz in Coq, Gonthier)


Erstes Bsp fuer externes Zertifikat:
------------------------------------

  A x <= b =>  c^T x <= d   

aequivalent zu

  max { c^T x | A x <= b } <= d

  loesbar mit SIMPLEX (lineare programmierung)

aequivalent zu

  exists r >= 0.  r^T A = c^T & r^T b <= d

  (<== weil r^T A x <= r^T b)
  (==> Farkash-Lemma;  r kann durch lin.prog. berechnet werden)

Also ist r ein Zertifikat.


Zweites Bsp fuer externes Zertifikat:  Primzahl-Zertifikat
----------------------------------------------------------

Satz von Pocklington (1914)

  n prim   gdw.   exists p1...pk a1..ak a  so dass
    1) p1..pk prim
    2) p1^a1 * ... * pk^ak teilt n-1 
    3) a^(n-1) = 1 (mod n)
    4) gcd (a^(n-1/pi)-1, n) = 1
    5) p1^a1 * ... * pk^ak > sqrt(n) ?!

Drittes Bsp:  CAD (cylindric algebra decomposition)
offenes Problem: Zertifikat dafuer?