MaLo - Advanced Formelzettel PDF

Preview

Summary

Normalformen Eine reduziert, wenn sie nur die Junktoren und den Quantor verwendet. Normalisierung durch und Quantorenregel. Mathematische Logik Merkzettel Eine ist in Negationsnormalform, wenn sie nur aus Literalen (X, und den Junktoren und den Quantoren aufgebaut ist. (Keine Negation bei Literalen)...

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 ,...