Was bisher geschah: klassische Aussagenlogik klassische Aussagenlogik: Syntax, Semantik Äquivalenz zwischen Formeln ϕ≡ψ gdw. Mod(ϕ) = Mod(ψ) wichtige Äquivalenzen, z.B. Doppelnegation-Eliminierung, DeMorgan-Gesetze, Distributivgesetze Junktorbasen, z.B. {¬, ∨, ∧}, {¬, ∨}, {¬, ∧}, {¬, →} Normalformen: NNF, CNF, DNF 46 Weitere Junktoren zweistelliger Junktor NAND (Sheffer-Funktion, ↑) mit p NAND q ≡ ¬(p ∧ q): W(p) W(q) W(p NAND q) 0 0 1 1 1 0 0 1 1 1 1 0 W(p NAND q) = 1−min(W(p), W(q)) {NAND} ist eine Junktorbasis. zweistelliger Junktor NOR (Peirce-Funktion, ↓) mit p NOR q ≡ ¬(p ∨ q): W(p) W(q) W(p NOR q) 0 0 1 0 1 0 0 0 1 1 1 0 W(p NOR q) = 1−max(W(p), W(q)) {NOR} ist eine Junktorbasis. 47 Boolesche Funktionen und Schaltungen Ziel: technische Realisierung Boolescher Funktionen gegeben: Boolesche Funktion f : {0, 1}n → {0, 1} Jede Boolesche Funktion kann durch unendlich viele aussagenlogische Formeln dargestellt werden. Entwurf einer aussagenlogischen Formel ϕ mit Semantik f . Spezifikation, Entwurf, Verifikation und Optimierung von Schaltungen finden auf logischer Ebene statt. 48 Logische Gatter Operation Junktor Negation ¬ Konjunktion ∧ Disjunktion ∨ NAND ↑ NOR ↓ Antivalenz XOR Gatter 1 & ≥1 & ≥1 =1 49 Logik Schaltungstechnik Junktoren Atome aussagenlogische Formeln logische Gatter Eingänge Schaltungen Beispiel: (¬p ∨ q) ∧ (¬r ∨ ¬q) Übersetzung Formelbaum – Schaltung (Tafel) 50 Realisierung Boolescher Funktionen gegeben: Boolesche Funktion f : {0, 1}n → {0, 1} gesucht: Realisierung von f als Schaltung Schritte zum Schaltungsentwuf: 1. Suche nach aussagenlogischer Formel ϕ mit Semantik f 2. Übersetzung von ϕ in eine Schaltung Beispiel: x1 x2 0 0 0 0 0 1 0 1 1 0 1 0 1 1 1 1 x3 0 1 0 1 0 1 0 1 f (x1 , x2 , x3 ) 0 0 1 Formel ϕ = (x2 ∧ ¬x3 ) ∨ (x1 ∧ ¬x2 ) 0 1 1 1 0 51 Optimierungsmöglichkeiten Schaltungen mit möglichst wenigen Gattern (kleine Formeln) möglichst wenigen verschiedenen Gattertypen (Junktorbasen mit wenigen Elementen, z.B. NAND-Gatter) fester Struktur, z.B. Tiefe (Normalformen) technische Realisierung und Anwendungen in der Vorlesung Computerarchitektur und -peripherie 52 Schaltungsentwurf gegeben: Boolesche Funktion f : {0, 1}n → {0, 1} Zu jeder Booleschen Funktion f : {0, 1}n → {0, 1} exisitieren unendlich viele Formeln ϕ ∈ AL({x1 , . . . , xn }) mit Semantik f . Normalformen DNF, CNF entsprechen zweistufigen Schaltnetzen. Umwandlung DNF in NAND-Form: 1. doppelte Negation der DNF, 2. Anwendung der deMorgan-Regel (CNF in NOR-Form analog) Vorteile der Normalformen: DNF und CNF: geringe Tiefe der Schaltung, daher kurze Signalwege NAND-Form: nur Gatter eines Typs 53 Wiederholung mi CNF Formeln der Form ni=1 j=1 li,j mit Literalen li,j heißen in konjunktiver Normalform. Beispiele: (¬p ∨ ¬q) ∧ (p ∨ q) ∧ ¬q, p ∨ q, p ∧ ¬q, ¬p mi DNF Formeln der Form ni=1 j=1 li,j mit Literalen li,j heißen in disjunktiver Normalform. Beispiele: ¬p ∨ (¬q ∧ p) ∨ (p ∧ q), p ∨ q, p ∧ ¬q, ¬p Zu jeder Formel ϕ ∈ AL(P) existieren eine äquivalente Formel ϕ2 ∈ AL(P) in CNF und eine äquivalente Formel ϕ3 ∈ AL(P) in DNF. 54 Kanonische Normalformen CNF ni=1 ϕi heißt kanonisch gdw. in jeder Disjunktion ϕi jede Aussagenvariable vorkommt. DNF ni=1 ϕi heißt kanonisch gdw. in jeder Konjunktion ϕi jede Aussagenvariable vorkommt. Minterme : Konjunktionen in einer kanonischen DNF Maxterme : Disjunktionen in einer kanonischen CNF Satz Zu jeder Formel ϕ ∈ AL(P) existieren (bis auf Umordnung) eindeutige Formeln ϕ1 , ϕ2 ∈ AL(P) mit ϕ ≡ ϕ1 ≡ ϕ2 , wobei ϕ1 in kanonischer CNF und ϕ2 in kanonischer DNF. Die kanonischen CNF und DNF einer Formel ϕ lassen sich aus der Wahrheitswerttabelle der Formel ϕ ablesen. 55 Minimale CNF und DNF Wiederholung: varcount(ϕ) = Anzahl aller Variablenvorkommen in der Formel ϕ Eine DNF (oder CNF) ϕ heißt genau dann minimal, wenn für jede zu ϕ äquivalente DNF (oder CNF) ψ gilt: varcount(ϕ) ≤ varcount(ψ) Zu einer Formel können verschiedene äquivalente minimale DNF existieren. Beispiel: (a ∧ ¬b) ∨ (¬a ∧ (b ∨ c)) = (a ∧ ¬b) ∨ (¬a ∧ b) ∨ (¬a ∧ c) = (a ∧ ¬b) ∨ (¬a ∧ b) ∨ (¬b ∧ c) 56 DNF-Minimierungsproblem gegeben: Boolesche Funktion f : {0, 1}n → {0, 1} (als kanonische DNF ϕ) gesucht: minimale DNF ψ mit Semantik f (ϕ ≡ ψ) naiver Lösungsansatz: alle DNF mit weniger Variablenvorkommen testen theoretisch möglich, aber nicht sinnvoll (Zeitaufwand) Fakt Für alle p ∈ P und ψ ∈ AL(P) gilt (p ∧ ψ) ∨ (¬p ∧ ψ) ≡ ψ. Idee zur DNF-Minimierung: Umformung der DNF durch (evtl. mehrfache) Anwendung des Faktes. Beispiel (Tafel): (a ∧ ¬b ∧ ¬c) ∨ (a ∧ ¬b ∧ c) ∨ (¬a ∧ b ∧ c) ∨ (¬a ∧ ¬b ∧ c) 57