Vortragsfolien - tdi.informatik.uni

¨ hrung
Logik in der Informatik - Einfu
in die formale Logik
Sommersemester 2015
Prof. Dr. Isolde Adler
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Inhalt
2. Normalformen
2.1
2.2
2.3
2.4
Isolde Adler
¨
Aquivalenz
und Folgerung
Die pr¨
anexe Normalform
Termreduzierte Formeln
Relationale Signaturen
Logik – SoSe 2015
2/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Satz 2.4 (Satz u
¨ber die Pr¨anex-Normalform)
Jede FO[σ]-Formel ϕ ist ¨aqivalent zu einer FO[σ]-Formel ϕ0 in pr¨anexer
Normalform mit frei(ϕ) = frei(ϕ0 ).
Isolde Adler
Logik – SoSe 2015
3/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Inhalt
2. Normalformen
2.1
2.2
2.3
2.4
Isolde Adler
¨
Aquivalenz
und Folgerung
Die pr¨
anexe Normalform
Termreduzierte Formeln
Relationale Signaturen
Logik – SoSe 2015
4/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Beispiel 2.6
Sei σ = {f , g } und
2 1
ϕ = ∀x ∃y f (x, g (y )) = x.
Die Formel ϕ enth¨alt hier den geschachtelten“ Term f (x, g (y )). Man
”
sieht leicht, dass ϕ ¨aquivalent ist zu der Formel
ϕˆ = ∀x ∃y ∃z (g (y ) = z ∧ f (x, z) = x).
in der keine geschachtelten“ Terme vorkommen.
”
Isolde Adler
Logik – SoSe 2015
5/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Definition 2.7
Eine FO[σ]-Formel heißt termreduziert, wenn all ihre atomaren
Teilformeln von der Form
• R(x1 , . . . , xr ),
mit R ∈ σ, r = ar(R), x1 , . . . , xr ∈ Var
• f (x1 , . . . , xk ) = y ,
mit f ∈ σ, k = ar(f ), x1 , . . . , xk , y ∈ Var
• x = c,
mit x ∈ Var, c ∈ σ oder
• x = y,
mit x, y ∈ Var
sind.
Isolde Adler
Logik – SoSe 2015
6/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Satz 2.8
Jede FO[σ]-Formel ϕ ist ϕ ist ¨aquivalent zu einer termreduzierten
FO[σ]-Formel ϕ0 mit frei(ϕ) = frei(ϕ0 ).
Beweis.
– Siehe Tafel –
Isolde Adler
Logik – SoSe 2015
7/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Inhalt
2. Normalformen
2.1
2.2
2.3
2.4
Isolde Adler
¨
Aquivalenz
und Folgerung
Die pr¨
anexe Normalform
Termreduzierte Formeln
Relationale Signaturen
Logik – SoSe 2015
8/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Definition 2.9
Eine Signatur heißt relational, wenn sie keine Funktionssymbole und keine
Konstantensymbole enth¨alt.
Manchmal (z. B. in den Kapiteln 3 und 4) ist es vorteilhaft, sich auf
relationale Signaturen zu beschr¨anken. Im Folgenden zeigen wir, dass dies
keine wirkliche Einschr¨ankung ist, da man Funktionen und Konstanten
durch geeignete Relationen repr¨asentieren kann.
Isolde Adler
Logik – SoSe 2015
9/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Definition 2.10
– Siehe Tafel –
Isolde Adler
Logik – SoSe 2015
10/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Satz 2.11
(a) Zu jeder FO[σ]-Formel ϕ gibt es eine FO[σrel ]-Formel ϕ,
ˆ so dass f¨
ur
alle zu ϕ passenden Interpretationen (A, β) gilt:
(A, β) |= ϕ ⇐⇒ (Arel , β) |= ϕ.
ˆ
(b) Zu jeder FO[σrel ]-Formel ϕ gibt es eine FO[σ]-Formel ϕ,
ˆ so dass f¨
ur
alle zu ϕˆ passenden Interpretationen (A, β) gilt:
(Arel , β) |= ϕ ⇐⇒ (A, β) |= ϕ.
ˆ
Isolde Adler
Logik – SoSe 2015
11/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Beweis von Satz 2.11 (a). . .
(a) Zu jeder FO[σ]-Formel ϕ gibt es eine FO[σrel ]-Formel ϕ,
ˆ so dass f¨
ur
alle zu ϕ passenden Interpretationen (A, β) gilt:
(A, β) |= ϕ ⇐⇒ (Arel , β) |= ϕ.
ˆ
Gem¨aß Satz 2.8 gen¨
ugt es, ϕˆ f¨
ur termreduzierte FO[σ]-Formeln ϕ
anzugeben. Wir tun dies induktiv u
¨ber den Aufbau von ϕ.
Fall 1: ϕ hat die Form R(y1 , . . . , yr ) mit R ∈ σ, r = ar(R),
y1 , . . . , yr ∈ Var. Dann ist ϕˆ := ϕ.
Fall 2: ϕ hat die Form f (x1 , . . . , xk ) = y mit f ∈ σ, k = ar(f ),
x1 , . . . , xr , y ∈ Var. Dann ist ϕˆ := Rf (x1 , . . . , xk , y ).
Fall 3: ϕ hat die Form x = c mit c ∈ σ, x ∈ Var. Dann ist ϕˆ := Rc (x).
Fall 4: ϕ hat die Form x = y mit x, y ∈ Var. Dann ist ϕˆ := ϕ.
Isolde Adler
Logik – SoSe 2015
12/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
. . . Beweis von Satz 2.11 (a)
(a) Zu jeder FO[σ]-Formel ϕ gibt es eine FO[σrel ]-Formel ϕ,
ˆ so dass f¨
ur
alle zu ϕ passenden Interpretationen (A, β) gilt:
(A, β) |= ϕ ⇐⇒ (Arel , β) |= ϕ.
ˆ
Fall 5: ϕ hat die Form ¬ψ mit ψ ∈ FO[σ] und ψ ist termreduziert. Dann ist
ˆ
ϕˆ := ¬ψ.
Fall 6: ϕ hat die Form (ψ1 ∗ ψ2 ) mit ψ1 , ψ2 ∈ FO[σ], ∗ ∈ {∧, ∨, →, ↔} und
ψ1 , ψ2 ∈ FO[σ] sind termreduziert. Dann ist ϕˆ := (ψˆ1 ∗ ψˆ2 ).
Fall 7: ϕ hat die Form Qx ψ mit ψ ∈ FO[σ], Q ∈ {∀∃}, x ∈ Var und
ˆ
ψ ∈ FO[σ] ist termreduziert. Dann ist ϕˆ := Qx ψ.
Man sieht leicht, dass in jedem der oben angegebenen F¨alle f¨
ur jede zu ϕ
passende σ-Interpretation (A, β) gilt:
(A, β) |= ϕ ⇐⇒ (Arel , β) |= ϕ.
ˆ
Isolde Adler
Logik – SoSe 2015
13/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Beweis von Satz 2.11 (b)
(b) Zu jeder FO[σrel ]-Formel ϕ gibt es eine FO[σ]-Formel ϕ,
ˆ so dass f¨
ur
alle zu ϕˆ passenden Interpretationen (A, β) gilt:
(Arel , β) |= ϕ ⇐⇒ (A, β) |= ϕ.
ˆ
Zum Beweis k¨
onnen wir ¨ahnlich wie in (a) vorgehen, wobei wir an Stelle
von Fall 2 und Fall 3 folgendermaßen vorgehen.
Fall 20 : ϕ hat die Form Rf (x1 , . . . , xk , xk+1 ) mit k + 1 = ar(Rf ),
x1 , . . . , xr , xk+1 ∈ Var. Dann ist ϕˆ := f (x1 , . . . , xk ) = xk+1 .
Fall 30 : ϕ hat die Form Rc (x) mit x ∈ Var. Dann ist ϕˆ := x = c.
Isolde Adler
Logik – SoSe 2015
14/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Inhalt
3. Die Auswertungskomplexit¨at von FO in endlichen Strukturen
3.1 Die Auswertung von FO-Formeln
Isolde Adler
Logik – SoSe 2015
15/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Inhalt
3. Die Auswertungskomplexit¨at von FO in endlichen Strukturen
3.1 Die Auswertung von FO-Formeln
Isolde Adler
Logik – SoSe 2015
16/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Die Auswertung von FO-Formeln
Definition 3.1
Eine σ-Struktur A heißt endlich, wenn ihr Universium A nur endlich viele
Elemente enth¨alt.
Sei σ eine endliche relationale Signatur (d. h. σ besteht aus endlich vielen
Relationssymbolen). Als Eingabe f¨
ur Algorithmen repr¨asentieren wir eine
endliche σ-Struktur wie folgt:
• Die Elemente des Universums von A repr¨
asentieren wir durch
Objekte eines geeigneten Datentyps Θ (etwa integer oder string).
Das Universum A von A wird dann als Liste von Objekten vom Typ
Θ repr¨asentiert.
• Ein r -Tupel (a1 , . . . , ar ) ∈ Ar repr¨
asentieren wir als Liste von
Objekten vom Typ Θ. F¨
ur jedes R ∈ σ repr¨asentieren wir die
Relation R A dann als Liste aller r -Tupel (a1 , . . . , ar ) ∈ R A (f¨
ur
r := ar(R)).
Beachte: Die Repr¨asentation von A hat ungef¨ahr die Gr¨oße
X R A · ar(R).
|σ| + |A| +
R∈σ
Isolde Adler
Logik – SoSe 2015
17/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Definition 3.2.
Sei σ eine endliche relationale Signatur.
(a) Die Gr¨
oße kAk einer endlichen σ-Struktur A ist definiert als
X R A · ar(R).
kAk := |σ| + |A| +
R∈σ
(b) Die L¨ange kϕk (bzw. Gr¨
oße) einer FO[σ]-Formel ϕ ist definiert als
die L¨ange von ϕ als Wort u
¨ber dem Alphabet Aσ .
Isolde Adler
Logik – SoSe 2015
18/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Definition 3.3
Sei σ eine endliche relationale Signatur.
(a) FINσ bezeichnet die Klasse aller endlichen σ-Strukturen.
(b) FIN bezeichnet die Klasse aller endlichen σ-Strukturen, f¨
ur alle
endlichen relationalen Signaturen σ.
Isolde Adler
Logik – SoSe 2015
19/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Die Breite einer Formel
Beobachtung 3.5 f¨
uhrt unmittelbar zu einem rekursiven Algorithmus, der
das Auswertungs- problem f¨
ur FO auf FIN l¨asst. Die genaue Laufzeit des
Algorithmus h¨angt von dem folgenden Parameter ab:
Definition 3.7
Sei σ eine relationale Signatur. Die Breite (engl. width) br(ϕ) einer
Formel ϕ ∈ FO[σ] ist die maximale Anzahl freier Variablen in Subformeln
von ϕ, d.h.:
br(ϕ) = max |frei(ψ)| : ψ ∈ sub(ϕ) .
Isolde Adler
Logik – SoSe 2015
20/21
Die Auswertungskomplexit¨
at von FO in endlichen Strukturen
Normalformen
Beobachtung 3.8
(a) br(ϕ) ≤ kϕk
(b) br(ϕ) ≤ | var(ϕ)|
(c) F¨
ur jede FO[σ]-Formel ϕ gibt es eine zu ϕ ¨aquivalente FO[σ]-Formel
ϕ0 mit frei(ϕ0 ) = frei(ϕ), in der h¨
ochstens br(ϕ) viele verschiedene
Variablen vorkommen.
Beweis.
¨
Ubung
Isolde Adler
Logik – SoSe 2015
21/21

Download Report