Rechnergestütztes Beweisen (Hofmann, WS 2005/06)

2005-12-21 VL 19

Wdh: Nelson-Oppen
Vollständigkeit nur für Gleichungstheorien bewiesen.  Neu: derselbe
Beweis funktioniert für jede konvexe Theorie.  Dazu zeigen wir, dass
jede konvexe Theorie ein universelles Modell hat.

Def: Eine Theorie T is konvex, falls folgendes gilt:
     Sei Gamma eine Konjuktion von Gleichungen und
     Delta = OR { E1, ... , En} eine Disjunktion von Gleichungen.
     Wenn T |= Gamma => Delta, dann schon T |= Gamma => Ei für ein i.

Satz: Sei T konvex und Gamma eine Konjunktion von Gleichungen, so dass
Gamma konsistent.  Dann existiert ein Modell II und eine Bewertung
rho, so dass II |= T,  II,rho |= Gamma.  Für jede Gleichung E (mit
Variablen) gilt II,rho |= E gdw. T |= Gamma => E.

Beweis: Fasse alle Variablen als Konstanten auf.  Dann wird Gamma zu
einer geschlossenen Formel.

Setze M := T UNION Gamma UNION { NOT u=v | T |=/= Gamma => u=v }
(inspiriert von Ganzingers Korrektheitsbeweis der NO-Prozedur).

Beh.: Jede endliche Teilmenge von M hat ein Modell.  (Dann folgt mit
dem Kompaktheitssatz, dass M ein Modell hat.)

Sei o.B.d.A. T' = T UNION Gamma UNION { NOT ai=bi | i=1..n }.

Falls T |= OR_{i=1..n} ai=bi, dann existiert (Konvexität) ein i, so
dass T |= Gamma => ai=bi, im Widerspruch zur Herkunft der Gleichung.
Also gilt T |=/= Gamma => OR ai=bi, d.h. es existiert eine
Interpretation II, sodass II |= T, II |= Gamma, II |= NOT ai=bi für
alle i=1..n.  Also hat T' ein Modell.  Nach Kompaktheitssatz hat also
auch ganz M ein Modell II.  Setze rho(x) = II(c_x).  Es gilt II |= T,
II,rho |= Gamma, und II,rho |= NOT u=v gdw. T |=/= Gamma => u=v, also
II,rho |= u=v gdw. T |= Gamma => u=v.


Fallstudie: Verifikation eines Addierers

Bit = Boolean
Bitvektor = Folge von n bits.

bs = (b_{n-1}, ... , b1, b0) bedeuted die Zahl

bv2nat (bs) = SUM_{i=0..n-1} bi*2^i  
(wobei PVS booleans implizit nach nat konvertiert)

n-bit Addierer nimmt

* zwei Bitvektoren bs, cs
* ein Bit c_in (einlaufender Übertrag)

und produziert

* einen Bitvektor sum
* ein Bit c_out (auslaufender Übertrag)

so dass

  cout*2^n + bv2nat(sums) = bv2nat(bs) + bv2nat(cs) + cin

Für n=1 kann man das mit einem Volladdierer realisieren

  sum  = b + c + cin [+=XOR]
  cout = (b AND c) OR (b AND cin) OR (c AND cin)

Es gilt: sum + 2cout = b + c + cin 
                                  
Verschaltung (c_out) der (n-1)ten Einheit wird (c_in) der n-ten. 
Engl.:"ripple-adder".                  
                  

PVS:

IMPORTING bit %% datentyp bit=boolean, Konversion nach nat

  b2n(b:bool) : below(2) = IF b THEN 1 ELSE 0
  CONVERSION b2n

Recordtyp : [# carry: bit, sum: bit #]
Records   : (# carry := ..., sum := ... #)
Projektion: sum(bla), bla`sum

ripple_adder[N : posnat] : THEORY

  IMPORTING bv[N], bv_nat

  bvec : TYPE = [below(N) -> bit]

  fill(b:bit): bvec = LAMBDA(n):b

(induct-and-simplify "j" :theories "full_adder" :exclude "FA")