Zusammenfassung - Merkzettel Klausur PDF

Preview

Summary

Download Zusammenfassung - Merkzettel Klausur PDF

Description

Normalformen

• Eine FO-Formel heißt reduziert, wenn sie nur die Junktoren ∨, ¬ und den Quantor ∃ verwen durch De-Morgan und Quantorenregel.

Mathematische Logik - Merkzettel

• Eine FO-Formel ist in Negationsnormalform, wenn sie nur aus Literalen (X, ¬X ) und den Junk Quantoren ∃, ∀ aufgebaut ist. (Keine Negation außer bei Literalen). Normalisierung von außen • Eine FO-Formel heißt termreduziert, wenn sie nur Atome der Form Rx, f x = y und x = y ent mit Tiefe gr¨ oßer 1). Normalisierung durch Einf ¨ uhren neuer Variablen. Beispiel: R xyz hat Tie Tiefe 2 anex-Normalform, wenn sie bereinigt ist und die Quantoren alle • Eine FO-Formel ist in Pr ¨ Bereinigt heißt, dass jede Variable nur entweder frei oder gebunden ist, außerdem darf sie nicht sein. Transformation ¨ uber die Quantorenregeln.

Philipp Fischer

Aussagenlogik Verschiedenes • Aussagenlogisches Interpolationstheorem: Sei ψ → ϕ eine aussagenlogische Tautologie. Dann existiert eine aussagenlogische Formel ϑ mit τ (ϑ) ⊆ τ (ψ) ∩ τ (ϕ), sodass ψ → ϑ und ϑ → ϕ Tautologien sind • Das Erf¨ ullbarkeitsproblem f¨ur Formeln in DNF kann in linearer Laufzeit gel¨ost werden • Eine Formelmenge ist endlich axiomatisierbar, wenn eine endliche Formelmenge existiert, welche die gleichen Modelle hat • Sei Φ ⊆ AL eine Formelmenge und X ∈ τ (Φ) eine Aussagenvariable. X heißt explizit definierbar in Φ, wenn eine Formel ϕ ∈ AL existiert, welche X nicht enth¨alt, sodass Φ  X ↔ ϕ

Eigenschaften der Folgerungsbeziehung • {ψ, ϕ}  ψ ∧ ϕ • Φ ∪ {ψ}  ϕ und Φ ∪ {¬ψ }  ϕ dann gilt Φ  ϕ • ∅  ψ genau dann wenn ψ Tautologie

• Zu jeder Formel ψ existiert ein Formel ϕ in relationaler Skolem-Normalform die relational i ∀x1 . . . ∀x r∃y 1 . . . ∃ys η hat, sodass ψ und ϕ uber ¨ denselben Universen erf u ¨ llbar sind. (Die Sign tuell anders, da neue Relationen eingef¨ uhrt und Funktionen entfernt werden) Transformation Skolem-Normalform, dann Termreduktion, nach-außen-Wandern der Existenzquantoren und da Relationen, die die Funktionen beinhalten“ ” • Simultane Substitution: ϕ[x1 /l1 , . . . , x k/lk ]. Gebundene Variablen werden nicht ersetzt. Kollision werden durch Umbenennung der gebundenen Variablen gelo¨st

Spieltheorie

• Φ  ψ genau dann wenn Φ ∪ {¬ψ} unerf¨ullbar • Φ  ψ und Φ  ¬ψ dann ist Φ unerf¨ullbar. Unerf¨ullbare Formelmenge folgern jede beliebige Formel.

• Ein Spiel ist fundiert wenn es endlich ist. Es heißt determiniert, wenn von jeder Position aus ein eine Gewinnstrategie hat. Alle fundierten Spiele sind determiniert

• Zu einem FO-Satz ψ und einer passenden Struktur A wird das Auswertungsspiel MC(A, ψ ) defi • Eine Position des Spiels: (ϕ, β ), wobei ϕ Unterformel von ψ und β : frei(ϕ) → A

Horn-Formeln und Erf¨ ullbarkeitstest

• A  ψ genau dann, wenn die Verifiziererin eine Gewinnstrategie f¨ur das Spiel MC(A, ψ ) von d aus hat.

• Konjunktion von Disjunktionen (Klauseln) • Jede Klausel von der Form (1) ¬X1 ∨ . . . ∨ ¬X k ∨ X ≡ X1 ∧ . . . ∧ Xk → X (2) ¬X1 ∨ . . . ∨ ¬X k ≡ X1 ∧ . . . ∧ Xk → 0

ullbarkeits¨ aquivalent: Ein FO-Satz ψ la¨sst sich in Skolem-Normalform transformieren, soda • Nur erf¨ und ϕ  ψ und sodass zu jedem ψ -Modell ein ϕ-Modell existiert (als Expansion). Transformatio der Existenzquantoren und Ersetzen der Variable durch neue Funktionen, die abh¨angig von Allquantoren sind.

Modallogik

(oder 1 → X)

• Ein Transitionssystem bzw. eine Kripkestruktur: K = (V , (Ea)a∈A , (Pi )i∈I ) wobei E a ⊆ V × V (i ∈ I )

• Algorithmus zum Test der Erf ¨ullbarkeit: – Markiere zu Beginn alle X der Form 1 → X – Solange sich aus bereits markierten Variablen eine neue folgern ¨al sst, markiere diese. L¨ asst sich 0 folgern, so ist die Formel unerf¨ullbar. • Der Algorithmus findet das kleinste Modell von ψ

• K, υ  ψ heißt ψ gilt im Zustand υ von K • K, υ  haiψ wenn ein w existiert, zu dem man mit Transition a kommt und bei dem ψ gilt.

• K, υ  [a]ψ wenn f u ¨ r alle Nachbarn w zu denen man mit Transition a kommt ψ gilt. (Wenn kei • Die Extension von ψ in K wird definiert als [ψ ]K = {υ | K, υ  ψ } (Also alle Zusta¨nde in denen • [ P i] = P i • [ ¬ψ] K = V − [ ψ] K [ ψ ∧ ϕ] K = [ ψ ]K ∩ [ ϕ]K [ ψ ∨ ϕ] K = [ ψ ]K ∪ [ ϕ]K [ ψ → ϕ] K = (V − [ ψ] K) ∪ [ ϕ] K

Kompaktheitssatz und Derivate • Φ ist erf¨ ullbar ⇔ jede endliche Teilmenge von Φ ist erf ¨ullbar. • Φ  ϕ ⇔ es existiert eine endliche Teilmenge Φ0 ⊆ Φ mit Φ 0  ϕ • Ist Φ ¨aquivalent zu einer endlichen Formelmenge Ψ, so existiert auch eine endliche Teilmenge Φ0 ⊆ Φ die ¨ aquivalent zu Φ ist.

• [ haiψ] K = {v | vE a ∩ [ ψ ] K = 6 ∅}

Resolution

• [ [a]ψ] K = {v | vE a ⊆ [ ψ ] K } • Formel ist erf u ¨llbar, wenn es ein entsprechendes Transitionssystem und einen Zustand gibt, de ist g ¨ ultig, wenn K, υ  ψ f ¨ ur alle K, υ

Zum Nachweis der Unerf¨ullbarkeit von Formeln in KNF. Formel muss in Klauselform betrachtet werden.

• F¨ ur alle Formeln ψ, ϕ ∈ ML und alle Aktionen gilt:

• C ist Resolvente von C1 und C 2 wenn Y ∈ C1 und Y ∈ C2 und C = (C1 − {Y }) ∪ (C2 − {Y }) • Res(K ) = K ∪ {C | C ist Resolvente} S • Res∗ (K ) = n∈N Resn(K ) Eine spezielle Form der Resolution, die Einheitsresolution ist nur f¨ur Horn-Formeln vollst¨andig. Sie verwendet pro Resolutionsschritt immer mindestens eine Klausel mit nur einem Literal. Eine weitere Form, die P-Resolution bildet nur Resolventen aus Klauseln, wenn eine der beiden Klauseln nur positive Literale enth¨alt. Sie ist korrekt und vollst¨andig.

Sequenzenkalk¨ ul • Eine Sequenz: Antezedens ⇒ Sukzedens amisse und Konklusion. Eine Interpretation falsifiziert die Konklusion genau dann • Eine Schlussregel besteht aus Pr¨ wenn sie eine Pr¨amisse der Regel falsifiziert. Es folgt, dass die Konklusion genau dann g¨ultig ist, wenn die Pr¨ amissen g¨ultig sind V W V W • Γ ⇒ ∆ ist gultig, genau dann wenn Γ  ∆ genau dann wenn Γ ∧ ¬ ∆ unerf ¨ullbar. ¨

(¬ ⇒)

Γ ⇒ ∆, ψ Γ, ¬ψ ⇒ ∆

(⇒ ¬)

Γ, ψ ⇒ ∆ Γ ⇒ ∆, ¬ψ

(∨ ⇒)

Γ, ψ ⇒ ∆ Γ, ϑ ⇒ ∆ Γ, ψ ∨ ϑ ⇒ ∆

(⇒ ∨)

Γ ⇒ ∆, ψ, ϑ Γ ⇒ ∆, ψ ∨ ϑ

(∧ ⇒)

Γ, ψ, ϑ ⇒ ∆ Γ, ψ ∧ ϑ ⇒ ∆

(⇒ ∧)

Γ ⇒ ∆, ψ Γ ⇒ ∆, ϑ Γ ⇒ ∆, ψ ∧ ϑ

(→⇒)

Γ ⇒ ∆, ψ Γ, ϑ ⇒ ∆ Γ, ψ → ϑ ⇒ ∆

(⇒→)

Γ, ψ ⇒ ∆, ϑ Γ ⇒ ∆, ψ → ϑ

(⊕ ⇒)

Γ, ϕ, ¬ψ ⇒ ∆ Γ, ¬ϕ, ψ ⇒ ∆ Γ, ϕ ⊕ ψ ⇒ ∆

Γ ⇒ ∆, ϕ Γ ⇒ ∆, ψ (| ⇒) Γ, ϕ|ψ ⇒ ∆

(⇒ ⊕)

Γ ⇒ ∆, ϕ, ψ Γ ⇒ ∆, ¬ϕ, ¬ψ Γ ⇒ ∆, ϕ ⊕ ψ

Γ, ϕ, ψ ⇒ ∆ (⇒ |) Γ ⇒ ∆, ϕ|ψ

– haiψ → [a]ψ ist erf¨ ullbar aber nicht g¨ ultig – [a](ψ → ϕ) → ([a]ψ → [a]ψ) ist g u ¨ ltig at von hai und [a]) – [a]ψ ≡ ¬hai¬ψ (Dualit¨ • [a]ψ ≡ ¬hai¬ψ • Bisimilarit¨ at zweier Kripkestrukturen: K, u ∼ K′ , u′ • K, υ ∼ K ′ , υ′ dann K, υ ∼ nK ′ , υ ′ f u ¨ r alle n aber umgekehrt nicht • Modaltiefe: md(haiψ) = md([a]ψ) = md(ψ ) + 1 Bei Verzweigungen durch Junktoren z¨ ahlt das

• Aus K , u ∼ n K′ , u′ folgt K , u ≡nML K′, u ′ (F u ¨ r den unendlichen Fall auch ohne n; Umkehrung g endlich verzweigten Transitionssystemen) • Die Modallogik hat die Baummodelleigenschaft. Sie kann die abgewickelte Kripkestruktur nich lichen unterscheiden, da diese bisimilar sind.

Temporale Logiken LTL - Linear time Temporal Logic • Auswertung auf endlichen oder unendlichen W¨ ortern v 0 v1 . . . mit atomaren Aussagen P i • LTL-Formeln: Alle AL-Formeln u ¨ ber {Pi | i ∈ N} und die Ausdr¨ ucke Xψ und (ψ Uϕ) • Eine Formel ψ gilt an einem Punkt vi geschrieben als W, vi  ψ • W, vi  Xψ genau dann, wenn v i nicht das letzte Element von W ist und W, v i+1  ψ ur alle • W, vi  (ψ Uϕ) genau dann, wenn ein n ≥ i existiert, sodass W, vn  ϕ und W , vm  ψ f¨ • Fψ := (1Uψ ) (irgendwann gilt ψ) • Gψ := ¬F¬ψ (immer wird ψ gelten) • GFϕ wenn ϕ an unendlich vielen Positionen gilt • FG¬ϕ wenn ϕ nur an endlich vielen Positionen gilt • Einbettbar in FO in die Struktur W = (V ,...