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

2005-12-07 VL 15

Sei T eine Theorie für die die Frage

  T |= Gamma => E

entscheidbar ist (Gamma: Liste von Gleichungen, E: Gleichung).  T muss
nicht notwendigerweise Gleichungstheorie sein, wird aber als konvex
vorausgesetzt: 

  T |= FORALL xs. u1=v1 AND ... AND un=vn IMPLIES s1=t1 OR ... OR sm=tm

impliziert

  T |= FORALL xs. u1=v1 AND ... AND un=vn IMPLIES si=ti

für ein i.

Ziel: Entscheide die Erweiterung von T um uninterpretierte
Funktionssymbole.

1. Ackermann Methode
====================

Führe für jeden Teilterm f(ss), der mit einem Funktionssymbol beginnt,
eine Variable x_f(ss) ein und ersetzt alle Vorkommen von f(ss) durch
x_fss.  Führe zusätzliche Klauseln ein, die das Verhalten dieser
x-Variablen beschreiben. 

  s1=t1, ..., sn=tn => x_f(ss) = x_f(ts)

(sofern beide Variablen im Problem vorkommen).


1. Beispiel: f(x-1)-1=x+1, f(y)+1=y-1, y+1=x IMPLIES 0=1.

Zwei neue Variablen: a (für f(x-1)) und b (für f(y)).

Die ursprüngliche Frage ist äquivalent zu

  CONG, a-1=x+1, b+1=y-1, y+1=x IMPLIES 0=1

wobei CONG = ( x-1=y IMPLIES a=b )
           = NOT x-1=y OR a=b

Zu zeigen:

  (1) a=b, a-1=x+1, b+1=y-1, y+1=x IMPLIES 0=1
  (2) a-1=x+1, b+1=y-1, y+1=x IMPLIES 0=1 OR x-1=y

(1) folgt durch Einsetzung von b und x und Ausrechnen.
(2) x-1=y folgt aus y+1=x


2. Beispiel: f^5(x)=x, f^3(x)=x.

Neue Variablen: a=f^5(x), b=f^4(x), c=f^3(x), d=f^2(x), e=f(x).

CONG = { b=c => a=b, 
         b=d => a=c, 
         b=e => a=d,
         b=x => a=e,
         c=d => b=c,
         c=e => b=d,
         c=x => b=e,
         d=e => c=d,
         d=x => c=e,
         e=x => d=e }

Ursprüngliche Frage äquivalent zu
  
  CONG, a=x, c=x => e=x

Umformen in Klauselform führt auf 2^10 Klauseln.

(ZZ a=e oder c=e
 ZZ b=x oder d=x
 ZZ a=b oder b=c oder a=d oder c=d
 ZZ b=e oder d=e
 ZZ c=x

Beweis: c=x,b=e,a=d,d=x,c=e,e=x)


Nelson-Oppen-Verfahren
======================

Hintergrund: Kombination von Entscheidungsverfahren.  Im Allgemeinen
ist Kombination entscheidbarer Theorien unentscheidbar.  Es
funktioniert aber, wenn die Theorien keine Funktions- oder
Relationssymbole gemeinsam haben.  Anfragen können dann in die Form

  Gamma1 AND Gamma2 IMPLIES x=y

gebracht werden, wobei Gamma1 über Sprache von Theorie 1 und Gamma2
über Sprache von Theorie 2 gebildet ist.

Beispiel: car(cons(x+0,y)) = x   äquivalent zu

  z=car(cons(u,y)) AND u=x+0 IMPLIES z=x

Craigscher Interpolationssatz:  Es existiert eine quantorenfreie
Formel phi über der Sprache {=}, so dass

  Gamma1 IMPLIES phi  und
  phi AND Gamma2 IMPLIES x=y

genau dann wenn 

  Gamma1 AND Gamma2 IMPLIES x=y.

(Intuition: die Kommunikation zwischen Gamma1 und Gamma2 kann nur über
Gleichungen zwischen Variablen erfolgen, da die Sprachen sonst
verschieden sind.)

Idee des NO-Verfahrens:  Generiere systematisch Interpolanten phi.
Prüfe jeweils, ob

  Gamma1 IMPLIES phi  und
  phi AND Gamma2 IMPLIES x=y.

Spezialfall: Theorie 1 = T,  Theorie 2 = uninterpretierte FS.  Wir
betrachten jetzt eine Version von NO für diesen Spezialfall (Harald
Ganzinger, 2003).

Eine Konfiguration ist eine Sequenz  Gamma => E, wobei Gamma nur
Gleichungen s=t aus T oder "Definitionen" enthält, 
d.h., Gleichungen der Form f(u)=v, wobei wiederum u,v keine FS
enthalten.  E enthält auch keine unint. FS (d.h. E ist aus T).

Zu jeder Sequenz Gamma' => E' kann mit linearem Aufwand eine
äquivalente Konfiguration angegeben werden.

Beispiel: f^5(x)=x, f^3(x)=x => f(x)=x

f(a)=x, f(b)=a, f(c)=b, f(d)=c, f(x)=d, b=x => d=x

Ganzingers NO-Verfahren ist ein deduktives System, welches alle
Konfigurationen herleitet.  Die Regeln sind:

  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

Dieses Verfahren ist sicherlich korrekt: Hat eine Konfiguration eine
Herleitung, so ist sie auch wahr.

Beispiel: 

----------------------------------------- Ax
f(a)=x, f(b)=a, a=b, c=x, a=d, b=x => d=x
-------------------------------------------- Comp
f(a)=x, f(b)=a, f(c)=b, c=x, a=d, b=x => d=x
-------------------------------------------- Comp
f(a)=x, f(b)=a, f(c)=b, c=x, a=d, b=x => d=x
----------------------------------------------- Comp
f(a)=x, f(b)=a, f(c)=b, f(d)=c, a=d, b=x => d=x
-------------------------------------------------- Comp
f(a)=x, f(b)=a, f(c)=b, f(d)=c, f(x)=d, b=x => d=x


Vollständigkeit:  Wir zeigen, dass (1) auf jede wahre Konfiguration eine
Regel rückwärts angewendet werden kann und dass (2) die Regeln Wahrheit
reflektieren, d.h., wenn

  G' => E'
  -------- NO-Compose
  G => E

und G=>E wahr, dann G'=>E' wahr.  Da es keine unendlichen
Folgen von Rückwärtsanwendungen gibt (Zahl der der Definitionen nimmt
ab), folgt daraus die Vollständigkeit.

Zu (2): Sei II Modell von T, sei (*) Gamma, f(ss)=u, f(ts)=v => E wahr
(in T).  Ausserdem gelte II |= Gamma AND u=v AND f(ss)=u.  
Zu zeigen: II |= E
Wegen _Gamma => si=ti und II |= Gamma gilt: 
II |= si=ti, also II = f(ts)=u, also auch II |= f(ts)=v, da ja 
II |= u=v.  Somit II |= E aus (*).

Zu (1): Sei Gamma => E wahr in T.  Falls Gamma => E nicht Instanz von
NO-Axiom ist, also wenn T |=/= _Gamma => E, dann existiert ein Modell
II, so dass II |= _Gamma, aber nicht II |=/= E.  Gelänge es, alle FS
so zu interpretieren, dass die Def. auch wahr werden, so hätten wir
ein Gegenmodell zu Gamma => E.  Da das nicht sein kann, muss es zwei
konflingierende Definitionen geben, d.h., f(ss)=u, f(ts)=v, wobei
[|ss|]_II = [|ts|]_II, aber [|u|] =/= [|v|].