Rechnergestütztes Beweisen (Hofmann, WS 2005/06) 2005-11-30 VL 13 Gleichungstheorien ================== Motivation und Anwendung: Lineare Arithmetik + uninterpretierte Funktionssymbole Bsp 1: Zeige 0=1 aus f(x-1)-1 = x+1 f(y)+1 = y-1 y+1 = x Bsp 2: Zeige f(x)=x aus f^5(x)=x und f^3(x)=x Zwei Entscheidungsverfahren: ---------------------------- Nelson-Oppen: Kombination zweier (entscheidbarer) Gleichungstheorien, z.B. lin. Arith. und uninterp. F.S. Shostak: Kombination einer Gleichungstheorie mit uninterp. F.S. In seinem Anwendungsfeld besser als N.-O. Def. (Gleichung) Sei L eine Sprache und t1 und t2 zwei Terme, so dass K >L t1 : tau K >L t2 : tau Eine Gleichung ist ein formaler Ausdruck K >L t1 = t2 : tau kurz geschrieben als t1 = t2. Ist II Interpretation von L und t1=t2 eine Gleichung, so erfüllt II die Gleichung t1=t2, in Zeichen II |= t1 = t2, falls [|t1|]_II,rho = [|t2|]_II,rho für alle Belegungen rho. Def. (Gleichungstheorie) Eine Gleichungstheorie ist eine Menge von T von Gleichungen über einer Sprache L, die unter den folgenden Regeln abgeschlossen ist: (REFL) t=t in T (für alle (wohltypisierten) t). (SYM) Wenn t1=t2 in T, dann auch t2=t1 in T. (TRANS) Wenn t1=t2 und t2=t3 in T, dann auch t1=t3 in T. (CONG) Wenn ti=ui in T für i=1..n, dann auch f(t1..tn)=f(u1..un) in T. (SUBST) Wenn t1=t2 in T, dann auch t1(x:=u) = t2(x:=u) in T. Zu jeder Menge M von Gleichungen existiert eine kleinste Gl.th. T = mit M <= T (das ist einfach der Abschluss von M unter den 5 Regeln). Man schreibt M |- t = u falls t=u in . Bem. Ist II eine Interpretation, so ist Th(II) = { "t=u" | II |= t=u } eine Gleichungstheorie. Satz (Birkhoff). Zu jeder Gleichungstheorie T existiert eine Interpretation II, so dass T = Th(II). Diese Int. ist das universelle Modell von T. Beweis. Sei L_oo die Erweiterung von L durch unendlich viele Konstanten von jedem Typ. Identifiziere Variablen mit diesen neuen Konstanten. II wird wie folgt definiert: [|tau|] = { t | >L_oo t : tau }/~ wobei t1~t2 gdw. t1=t2 in T (*) [| f |]([t1]~..[tn]~) = [f(t1..tn)]~ (**) (*) wobei auf der rechten Seite die neu eingeführten Konstanten als Variablen aufgefasst werden. ~ ist Äquivalenzrelation wegen (REFL), (SYM), (TRANS). (**) Wohldefiniert wegen (CONG). Noch zu zeigen II |= t1 = t2 gdw. t1=t2 in T. "<=" Sei t1=t2 in T. Zeige [|t1|]_rho = [|t2|]_rho. Sei rho = x1->[u1]~,...,xn->[un]~ Dann [|t1|]_rho = [t1(x1:=u1,...,xn:=un)]~ (durch Induktion über t1) = [t2(x1:=u1,...,xn:=un)]~ (wegen SUBST) = [|t2|]_rho (durch Induktion über t2) "=>" Sei II |= t1 = t2. Setze rho(x)=[^x]~ wobei ^x die zu x gehörige neue Konstante ist. Dann gilt [|t1|]_rho = [t1(xi:=^xi)]~ (wieder durch Induktion über t1) = [|t2|]_rho = [t2(xi:=^xi)]~ (") Also t1=t2 in T. Beispiel: Sei L = {+,*,-,0,1} und T die Theorie der Ringe, d.h., T = , wobei M={Ringaxiome} (siehe Übung 5). Satz von Jacobson. Sei R ein Ring. Falls zu jedem x in R ein n > 1 existiert, so dass x^n = x (d.h. der Ring ist nilpotent), dann ist R kommuntativ (x*y=y*x). (Bem. diese Spezifikation ist keine Gleichungstheorie.) Speziallfall: Erfüllt ein Ring die Gleichung x*x*x=x, so ist R kommutativ. Folgerung aus Birkhoff: Es existiert eine Herleitung von x*y=y*x aus den Ringaxiomen und der Gleichung x^3=x mit den Gleichungsregeln (REFL--SUBST). Bew: Wende Satz von Jacobson auf das universelle Modell an. Herleitung für n=3 (Thierry Coquand): e1 = 1-u u=x^2 e2 = u(1-v) v=(1-x)^2 e3 = uv xy = (e1 + e2 + e3)xy = e1xy + e2xy + e3xy = e2y - e3y = e1yx + e2yx + e3yx = yx Satz (Konvexität). Sei T Gleichungstheorie. Seinen t1=u1,...,tn=un Gleichungen, so dass für jedes Modell II von T und Belegung rho ein i existiert, so dass [|ti|]_II,rho = [|ui|]_II,rho (D.h.: T |= FORALL xs. t1=u1 OR ... OR tn=un.) Dann existiert ein i, so dass ti=ui in T. (D.h. T |= ti=ui für dieses i.) Beweis: Betrachte das universelle Modell II von T und die "universelle Belegung" rho(x)=^x. Nach Voraussetzung existiert ein i, so dass [ti]~ = [|ti|] = [|ui|] = [ui]~ Bem: Man sagt, jede Gleichungstheorie ist konvex. Bsp: Die Theorie T der Bool'schen Werte ist nicht konvex, da gilt T |= FORALL x. x=true OR x=false aber weder FORALL x.x=true noch FORALL x.x=false. T ist eben keine reine Gleichungstheorie. Ziel: Gegeben Gleichungstheorie T. - Entscheide, ob t=u in T für eine Gleichung t=u. - Entscheide, ob T |= FORALL xs. t1=u1 AND ... AND tn=un IMPLIES t=u Def. Eine Gleichungstheorie T ist kanonisierbar, wenn eine berechenbare Funktion sigma : Terme -> Terme existiert, so dass (C1) sigma(t) = t in T (C2) Wenn t1 = t2 in T, dann ist sigma(t1)==sigma(t2) (identisch). Folgerung: Falls sigma(t1)=sigma(t2), dann t1 = t2 in T. (C1,TRANS)