Rechnergestütztes Beweisen (Hofmann, WS 2005/06) 2005-11-09 Beweis des Satzes von Herbrand: "=>" Sei II Modell von Phi. Dann [|phi(ts)|]_II = tt für alle phi(ts) in Pi_Phi. Damit eta (P(ts)) := [|P(ts)|]_II ist erfüllende Belegung für Pi. "<=" Sei eta erfüllende Belegung für Pi_Phi. Wir konstruieren eine Interpretation II wie folgt: * [|tau|]_II = { geschlossene Terme vom Typ tau } (Herbrand-Universum) * [|f|]_II(ts) = f(ts) * [|P|]_II(ts) <==> eta(P(ts)) = tt (Wobei P(ts) hier als Atom angesehen wird.) Es folgt: II ist Model von Phi. Anwendung des Satzes: Um festzustellen, ob eine Menge Phi von Formeln der Form FORALL(xs:taus).phi, mit phi quantorenfrei, ein Modell hat, genügt es zu testen, ob Pi = { phi(ts) | FORALL xs:taus.phi in Phi } erfüllbar ist, z.B. mit Resolution. Resolution für Prädikatenlogik: Voraussetzung: Alle Typen enthalten mind. 1 geschl. Term. Literal: Negierte oder nicht negierte atomare Formel i.a. mit freien Variablen. Klausel: Endliche Menge von Literalen { l1, ..., lk }. Wird verstanden als FORALL (xs:taus): l1 OR ... OR lk, wobei xs die freien Variablen in den li bezeichnet. Klauselmenge: Menge von Klauseln, verstanden als Konjunktion. (Beachte: (FORALL x. phi AND psi) <==> (FORALL x. phi) AND (FORALL x. psi)) Regeln: K_1 OR l K_2 OR NOT l ------------------------- RES K_1 OR K_2 K t (evtl. offener) Term vom passenden Typ -------------------------------------------- INST K(x:=t) Beide Regeln sind korrekt im folgenden Sinne: Erfüllt II sowohl K_1 OR l als auch K_2 OR NOT l, dann auch K_1 OR K_2. Ebenso: Erfüllt II die Klausel K, so auch K(x:=t). (Bemerkung: wenn t keine Variable ist, ist die Aussage K(x:=t) sogar echt schwächer als K.) Folgerung aus dem Satz von Herbrand: Die Klauselmenge CC hat kein Modell gdw. aus CC mit RES und INST die leere Klausel herleitbar ist. Hierfür genügen schon die Spezialfälle: * RES nur wenn keine freien Variablen vorhanden. * INST nur für geschlossene Terme t. Setze Phi = Formelmenge, die CC entspricht. Falls Pi_Phi im Sinne von Herbrand inkonsistent ist, so existiert Herleitung der leeren Klausel im propositionalen Resolutionskalkül. Spiele diese Herleitung nach mit INST (zur Erzeugung der beteiligten Formeln) und RES (für die Resolutionsschritte). Beispiel: (x,y,r sind Variablen) K1 = { NOT S(r), NOT A(r,x,y), A(r,y,x) } K2 = { A(r,f(r),g(r)), S(r) } K3 = { NOT A(r,g(r),f(r)), S(r)} K4 = { S(s()) } K5 = { A(s(),a(),b())} K6 = { NOT A(s(),b(),a()) } --- K7 = { NOT A(r,x,y), A(r,y,x), A(r,f(r),g(r)) } (aus K1 und K2) K8 = { NOT A(s(),x,y), A(s(),y,x) } (aus K1 und K4) K9 = { A(s(),b(),a()), A(s(),f(s()),g(s()) } (aus K7 und K5) K11= { A(s(),b(),a()) } (aus K8 und K5) BOX (aus K11 und K6) In der Praxis wird INST immer direkt vor RES angewandt, und zwar gerade so stark, dass ein passendes Literal ensteht. Man kombiniert die beiden Regeln zu einer Regel K1 OR P(s1,...,sn) K2 OR NOT P(u1,...,un) sigma,tau Substitutionen --------------------------------------------- si(sigma) = ui(tau) K1(sigma) OR K2(tau) für all i=1...n Man wählt sigma, tau ohne Beschränkung der Vollständigkeit als "allgemeinster Unifikator" von ss und us. Definition (allgemeinster Unifikator): Seien ss, ts Tupel von Termen mit freien Variablen. (sigma,tau) bildet allgemeinsten Unifikator von ss und ts (in Zeichen (sigma, tau) = mgu(ss,ts)), wenn * ss(sigma) = ts(tau) * Falls ss(sigma') = ts(tau') dann ergeben sich sigma' und tau' durch Spezialisierung aus sigma und tau, d.h., es gibt eine Substitution rho mit sigma' = sigma(rho) tau' = tau(rho) Beispiel: s=f(x,g(y)) und u=f(h(y),x) mgu(s,t) ist (sigma,tau) mit sigma = (x:=h(y), y:=z) tau = (x:=g(z), y:=y). (*) Schöner s=f(x,g(y)) und u=f(h(j),k) mgu(s,t) ist (sigma,tau) mit sigma = (x:=h(z), y:=w) tau = (j:=z, k:=g(w)). Bemerkung:s=f(x,g(y)) und u=f(h(y),x) sind auch durch sigma'= (x:=h(y), y:=y) tau' = (x:=g(y), y:=y) unifizierbar, aber das ist nicht die allgemeinste Unifikation, sondern sie entsteht aus (*) durch die Spezialisierung rho=(z:=y). Umwandeln beliebiger Formeln der Prädikatenlogik in Klauseln: Skolemisierung. Identitäten (seien alle Typen nichtleer): (FORALL x.phi) => psi <==> EXISTS x. phi => psi (EXISTS x.phi) => psi <==> FORALL x. phi => psi (Qx.phi) * psi <==> Qx. phi * psi (*=AND,OR) (Q=ALL,EX) NOT (Qx.phi) <==> Qquer x. NOT phi Folgerung: Jede geschlossene Formel phi ist äquivalent zu einer Formel der Gestalt Q1(x1:tau1)...Qn(xn:taun).psi wobei Qi in {FORALL, EXISTS} und psi quantorenfrei. Diese Form heißt Pränex-Form (engl. prenex). Beobachtung: Sei phi = FORALL(xs:taus). EXISTS(y:tau').psi (psi beliebig) eine Formel mit Existenzquantor. phi hat ein Modell gdw. phi' := FORALL(xs:taus).psi(y:=f(xs)) wobei f ein frisches Funktionssymbol ist. Beispiel: TT = { elt, umg} PP = { enth : [elt,umg -> boolean] } FF = { f : [elt -> elt] } stetig(f) :<==> FORALL x:elt FORALL U:umg. enth(f(x),U) => EXISTS V:umg. enth(x,V) AND FORALL y:elt. enth(y,V) => enth(f(y),U) stetig(f) => stetig(f o f)