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

2005-12-08 VL 16

Wdh: Ganzinger's Verfahren

  T |= _Gamma => E            (_Gamma ist Gamma ohne Def.)
  ---------------- NO-Axiom
  Gamma => E

  T |= _Gamma => si = ti (für alle i)
  Gamma, u=v, f(ss)=u => E
  ---------------------------- NO-Compose
  Gamma, f(ss)=u, f(ts)=v => E

Konsequenz aus der Vollständigkeit:

1) Jede herleitbare Konfiguration ist gültig
2) Jede Auswahlstrategie für Rückwärtsanwendung liefert
Entscheidungsverfahren

Fortsetzung des Vollständigkeitsbeweises:

Noch zu zeigen: Auf jede gültige Konfiguration kann eine Regel
rückwärts angewandt werden.  Sei Gamma => E gültig.

Fall 1:  T |= _Gamma => E, dann ist Gamma => E Konklusion von
NO-Axiom.

Fall 2:  T |=/= _Gamma => E 

Falls T Gleichungstheorie ist, fasse Variablen in Gamma als Konstanten
auf und betrachte universelles Modell II von T UNION _Gamma.  Es gilt,
dass II |= a = b gdw. T |= _Gamma => a = b.  Nach Annahme II |=/= E.
Das Modell II lässt sich nicht zu einem Modell von Gamma erweitern, da
II |= E im Widerspruch zu T |=/= _Gamma => E.  Also gibt es
Definitionen f(ss) = u, f(ts) = v in Gamma mit II |= ss = ts, aber
II |=/= u=v.  Das bedeutet wegen Universalität, dass T |= _Gamma =>
si=ti.  D.h. NO-Compose anwendbar.

Falls T konvex ist, aber nicht notwendigerweise eine
Gleichungstheorie: Siehe eine zukünftige Version des Skriptes.


Gleichungslösen
===============

Gleichungslösen: Eine zentrale Method zur Entscheidung von
Implikationen von Gleichungen.

Def: Eine Theorie T ist lösbar, wenn ein Algorithmus Solve existiert,
der zu einer gegebenen Gleichung s=t entweder BOT (_|_) zurückgibt,
oder eine endliche Menge von Gleichungen x_1=u_1,...,x_n=u_n, wobei
x_1,...,x_n die Variablen in s und t sind.  Bedingungen:

* Die x_i dürfen nicht in den u_j vorkommen, die u_j dürfen aber neue
  Variablen enthalten.

* Solve(s=t)=BOT gdw. T |= s=t => x=y für frische x=y

* Solve(s=t) = {x1=u1(ps) ... xn=un(ps)} impliziert, dass in jedem
  Modell II von T gilt

     s=t <=> EXISTS ps. x1=u1(ps) AND ... AND xn=un(ps)


Beispiel: s=x+y-z 
          t=y-x+5

Solve(s=t) = { x=q, y=p, z=2q-5 }

Beispiel: T Gleichungstheorie von {true, false, if-then-else}
Falls true=false, dann

  x = if x then true else false = if x then true else true  = true =
    = if y then true else true  = if y then true else false = y

oder

  x = if true then x else y = if false then x else y = y


Lemma.  Solve(s=t) = { xi=ui(ps) | i=1..n }

     T |= (FORALL xs. s=t => phi(xs)) IFF
          (FORALL ps. phi(u1(ps)..un(ps)))

Beweis: Direkt aus Spezifikation von Solve.

Anwendung:  Sei T lösbar und kanonisierbar.  Dann ist die Frage T |=
Gamma => E entscheidbar.  Löse Gleichungen in Gamma sukzessive auf und
setze ein.  Falls BOT erscheint, so gilt Gamma => E trivial.
Andernfalls verbleibt eine unbedingte Gleichung, die mit der
Kanonisierung entschieden wird.


Beispiele für lösbare Theorien:

1. Lineare Arithmetik über Q. Sprache: 1:T, +:[T,T->T] und q*:[T->T]
für jedes q aus Q.  Die L.A., entweder als Gleichungstheorie, oder als
erststufige Theorie, ist lösbar (Schule).

Normalform von Termen:

  q1*x1 + ... + qn*xn + q(n+1)*1

Normalform von Gleichungen

  t = 0*1

Lösung von 

  q1*x1 + ... + qn*xn + q(n+1)*1 = 0

ist { x1 = (q1^-1)*(q2*y2 + ... + qn*yn + q(n+1)*1), xi=yi für i>1 }

Lösung von 1=0 ist BOT.

2. Paare und Projektionen.  Solve(x.1=y.2) = {x=<p,q>, y=<r,p>}.

3. Booleans + if-then-else.

4. Listen mit cons, car, cdr (Shostak zeigt Konvexität und
Lösbarkeit). (Haarige Geschichte.)
Solve(x=cons(y,x)) = BOT. Allerdings gibt es Modelle der
Gleichungstheorie, die diese Gleichung wahrmachen.  Die reine
Gleichungstheorie ist also nicht lösbar.  Welche Theorie dann?
Theorie erster Stufe?  Nicht konvex, da gilt:

  x = null OR x = cons(car x, cdr x)

5. T = Polynome von C nicht lösbar.  Was ist Lösung von x^2+y^2=1?
Intendierte Lösung x=sin(phi), y=cos(phi), aber sin, cos sind nicht in
L.  Trotzdem ist Implikation von Gleichungen mit Gröbner-Basen lösbar.


Shostak-Algorithmus
===================

Shostak-Algorithmus: Verfeinerung von NO für lös- und kanonisierbare
Theorie T.  (Sei sigma der Kanonisierer).

Konfiguration: S | Gamma => E, so dass

* S UNION Gamma ist eine NO-Konfiguration.

* S besteht aus reinen Gleichungen der Form x=u.  
  D.h. S=x1=u1...xn=un und keines der xi kommt in den uj vor und uj
  enthält keine uninterpretierten FS.

S | Gamma => E gültig  gdw.  S UNION Gamma => E gültig.


Regeln für "Shostak Light":


  SL-Axiom-R ---------------- falls sigma(s)=sigma(t)
             S | Gamma => s=t

  SL-Axiom-L ------------------- falls Solve(s=t) = BOT
             S | Gamma, s=t => E

             S,L | Gamma => E
  SL-Solve   ------------------- falls Solve(s=t) = L (=/= BOT)
             S | Gamma, s=t => E
  
             S, x=u | {u/x}(Gamma => E)
  SL-Reduce  --------------------------  {u/x} bezeichnet die Übersetzung
             S, x=u | Gamma => E         mind. eines Vorkommens von x durch u

             S | Gamma, f(ss)=u, u=v => E
  SL-Compose -------------------------------- falls sigma(ss)=sigma(ts)
             S | Gamma, f(ss)=u, f(ts)=v => E


Korrektheit und Vollständigkeit:

- Regeln erhalten und reflektieren Gültigkeit

- Rückwärtsanwendung terminiert, aber nur, wenn bei Anwendung von
Solve die Gleichung s=t nicht mit S reduziert werden kann.

- Auf gültige Konfiguration ist immer eine Regel rückwärts anwendbar.
Falls S | Gamma => E gültig, dann ist S UNION Gamma => E Konklusion
einer NO-Regel.

Beispiel: 

Axiom-L
...
y=p-1, x=p | f(p-1)=a, a-1=p+1, a=b, b+1=p-2 => 0=1
-------------------------------------------------------- Compose
y=p-1, x=p | f(p-1)=a, a-1=p+1, f(p-1)=b, b+1=p-2 => 0=1
-------------------------------------------------------- Reduce
y=p-1, x=p | f(x-1)=a, a-1=x+1, f(y)=b, b+1=y-1 => 0=1
------------------------------------------------------ Solve
0 | f(x-1)=a, a-1=x+1, f(y)=b, b+1=y-1, y+1=x => 0=1