Grundlagen der Informatik -

Was bisher geschah
Signatur Σ = (ΣF , ΣR )
z.B. ΣF =
{(apfel, 0), (banane, 0), (kirsche, 2), (pflaume, 2)}
Σ-Struktur A = (A, J·KA )
z.B. Σ-Struktur S = (S, J·KS ) mit S = ,
JapfelKS = 5, JbananeKS = 3,
JkirscheKS (x, y ) = x + y , JpflaumeKS (x, y ) = x · y
N
Variablen X
Terme Term(ΣF , X ), Grundterme Term(ΣF , ∅)
z.B. pflaume(apfel, kirsche(banane, apfel)) ∈
Term(ΣF , ∅)
Wert in Σ-Struktur A = (A, J·KA )
I eines Grundtermes t: Element JtKA ∈ A
Äquivalenz von Grundtermen in einer Struktur A
s ≡A t gdw. JsKA = JtKA
Interpretation von Termen mit Variablen
Signatur Σ = (ΣF , ΣR ), Variablenmenge X
Menge Term(ΣF , X ) aller Terme mit Variablen aus X
Σ-Struktur S = (S, J·KS )
Variablenbelegung β : X → S
Interpretation (für einen ΣF -Term mit Variablen aus X ):
Paar (A, β) aus einer Σ-Struktur A = (A, J·KA ) und einer
Variablenbelegung β : X → A
Wert des ΣF -Termes t = f (t1 , . . . , tn ) ∈ Term(ΣF , X ) in der
Interpretation (A, β):
falls t ∈ X (Variable), dann JtK(A,β) = β(x), sonst
JtK(A,β) = Jf KA Jt1 K(A,β) , . . . , Jtn K(A,β)
Beispiele
Signatur Σ = (ΣF , ΣR ) mit
ΣF = {(a, 0), (b, 0), (f , 1), (g, 2), (h, 2)} und ΣR = ∅
Variablenmenge X = {x, y }
Σ-Struktur S = (S, J·KS ) mit
S =
JaKS
JbKS
N
= 5
= 3
Jf KS (a) = 1 + a
JgKS (a, b) = a + b
JhKS (a, b) = a · b
Variablenbelegungen
β : {x, y } →
γ : {x, y } →
N mit β(x) = 0, β(y ) = 1
N mit γ(x) = 2, γ(y ) = 0
Terme s = g(h(f (a), x), h(x, y )) und t = h(f (x), g(y , a))
JsK(S,β) , JtK(S,β) , JsK(S,γ) , JtK(S,γ) (Tafel)
Atome – Syntax
Atom elementare Formel,
repräsentiert Eigenschaften von oder
Beziehungen zwischen Objekten
Signatur Σ = (ΣF , ΣR )
Menge aller Σ-Atome mit Variablen aus Menge X :
Atom(Σ, X ) = {R(t1 , . . . , tn ) | (R, n) ∈ ΣR und t1 , . . . , tn ∈ Term(ΣF , X )
Atome – Beispiele
I
Signatur Σ = (ΣF , ΣR ) mit
√
ΣF = {(1, 0), (2, 0), ( , 1), (+, 2)}
ΣR = {(=, 2), (≤, 2)}
Variablenmenge X = {x, y , z}
I
I
I
I
√
√x = 2 ∈ Atom(Σ, X )
√
p√ X ) (aber x + 2 ∈ Term(ΣF , X ))
px + 2√ 6∈ Atom(Σ,
1+ 2≤
2 ∈ Atom(Σ, X )
Signatur Σ = (ΣF , ΣR ) mit
ΣF = {(apfel, 0), (banane, 0), (kirsche, 2), (pflaume, 2)}
ΣR = {(erbse, 1), (tomate, 2)}
Variablenmenge X = {x, y }
I
I
I
I
y 6∈ Atom(Σ, X )
erbse(apfel) ∈ Atom(Σ, X )
erbse(tomate(apfel, kirsche(x, y ))) 6∈ Atom(Σ, X )
tomate(kirsche(apfel, apfel), x) ∈ Atom(Σ, X )
Prädikatenlogik (der ersten Stufe) – Syntax
aussagenlogische Junktoren t, f, ¬, ∨, ∧, →, ↔
neu: Σ-Atome, Quantoren ∀, ∃
Definition (induktiv)
Die Menge FO(Σ, X ) aller Formeln der Prädikatenlogik (der
ersten Stufe) über der Signatur Σ mit (Individuen-)Variablen
aus der Menge X ist definiert durch:
1. alle Atome R(t1 , . . . , tn ) ∈ Atom(Σ, X ) sind Formeln,
(Atom(Σ, X ) ⊆ FO(Σ, X ))
2. sind ∗ ein n-stelliger Junktor und ϕ1 , . . . , ϕn Formeln,
dann ist auch ∗(ϕ1 , . . . , ϕn ) eine Formel,
(Aus {ϕ1 , . . . , ϕn } ⊆ FO(Σ, X ) folgt ∗(ϕ1 , . . . , ϕn ) ∈ FO(Σ, X ))
3. ist ϕ eine Formel und x ∈ X eine (Individuen-)Variable,
dann sind auch ∀xϕ und ∃xϕ Formeln.
(Aus ϕ ∈ FO(Σ, X ) und x ∈ X folgt {∀xϕ, ∃xϕ} ⊆ FO(Σ, X ))
(Baumstruktur, analog zur Definition von Termen)
Beispiele
I
Σ = (ΣF , ΣR ) mit
ΣF = {(a, 0), (f , 1)}
ΣR = {(P, 1), (R, 2)}
X = {x, y }
Formeln aus FO(Σ, X )
ϕ1 = R(x, a)
ϕ2 = P(f (x))
ϕ3 = (P(x) ↔ (¬P(f (x)) ∧ (∀x∃y ((P(x) ↔ P(y )) ∧ R(x, y )))))
ϕ4 = ∀x∀y ϕ3
I
Σ = (∅, ΣR ) mit ΣR = {(p, 0), (q, 0)}
Formeln aus FO(Σ, ∅)
ψ1 = p ∨ q
ψ2 = ¬p ∨ ¬(q ∨ p)
(Spezialfall: Syntax der Aussagenlogik)
Variablen in Formeln
Wiederholung Teilformel
Vorkommen einer Individuenvariablen x in
I
Term t, falls t = x oder t = f (t1 , . . . , tn ) und x in einem ti
vorkommt
I
Atom a = p(t1 , . . . , tn ), falls x in einem ti vorkommt
I
Formel ϕ, falls x in einem Atom in ϕ
(Teilformel von ϕ, die Atom ist) vorkommt.
Vorkommen von x in ϕ heißt
gebunden , falls x in einer Teilformel von ϕ der Form ∃xψ
oder ∀xψ vorkommt,
bvar(ϕ) Menge aller gebundenen Variablen in ϕ
freie , sonst
fvar(ϕ) Menge aller freien Variablen in ϕ
im Allgemeinen gilt fvar(ϕ) ∩ bvar(ϕ) 6= ∅
Beispiele
ϕ1 = R(x, a)
bvar(R(x, a)) = fvar(R(x, a)) = {x}
ϕ3 = (P(x) ↔ (¬P(f (x)) ∧ (∀x∃y ((P(x) ↔ P(y )) ∧ R(x, y )))))
bvar(ϕ3 ) = {x, y }, fvar(ϕ3 ) = {x}
ϕ4 = ∀x∀y ϕ3
bvar(ϕ4 ) = {x, y }, fvar(ϕ4 ) = ∅
Sätze
Formel ϕ ∈ FO(Σ, X ) mit fvar(ϕ) = ∅ heißt Satz.
für ϕ ∈ FO(Σ, X ) mit fvar(ϕ) = {x1 , . . . , xn }
universeller Abschluß ∀ϕ := ∀x1 · · · ∀xn ϕ
existentieller Abschluß ∃ϕ := ∃x1 · · · ∃xn ϕ
Fakt
Für jede Formel ϕ ∈ FO(Σ, X ) sind ∀ϕ und ∃ϕ Sätze.
Variablenbelegungen und Interpretationen
Signature Σ, Variablenmenge X
Σ-Struktur S = (S, J·KS )
Belegung β : X −→ S der Variablen aus X in S
modifizierte Belegung β[x 7→ a] : X −→ S mit
a
für y = x
β[x 7→ a](y ) =
β(y ) sonst
Σ-Interpretation (S, β) mit
I
I
Σ-Struktur S = (S, J·KS )
Variablenbelegung β : X −→ S
modifizierte Interpretation (S, β[x 7→ a])
Wert in Interpretationen
Wert in Σ-Interpretation (S, β) mit S = (S, J·KS )
I
I
I
I
einer Individuenvariable x ∈ X : JxK(S,β) = β(x) ∈ S
eines Termes t = f (t1 , . . . , tn ) ∈ Term(Σ
F , X ):
JtK(S,β) = Jf KS Jt1 K(S,β) , . . . , Jtn K(S,β) ∈ S
eines Atomes a = p(t1 , . . . , tn ) ∈ Atom(Σ, X ):
JaK(S,β) = JpKS (Jt1 K(S,β) , . . . , Jtn K(S,β) ) ∈ {0, 1}
einer Formel ϕ ∈ FO(Σ, X ):
J¬ϕK(S,β) = 1 − JϕK(S,β)
Jϕ ∨ ψK(S,β) = max(JϕK(S,β) , JψK(S,β) )
Jϕ ∧ ψK(S,β) = min(JϕK(S,β) , JψK(S,β) )
J∀xϕK(S,β) = min{JϕK(S,β[x7→a]) | a ∈ S}
J∃xϕK(S,β) = max{JϕK(S,β[x7→a]) | a ∈ S}
Beispiele
Σ = (ΣR , ΣF ) mit ΣF = {(f , 1)},ΣR = {(R, 2)}, X = {x, y , z}
ϕ = R(x, y ) ∧ ∃zR(z, z)
I
I
ψ = ∀x∃yR(x, f (y ))
Σ-Struktur A = (A, J·KA ) mit A = {a, b, c}
Jf KA (a) = Jf KA (b) = c, Jf KA (c) = a
JRKA = {(a, a), (b, a), (a, c)}
Belegung α(x) = b, α(y ) = a , α(z) = b
JϕK(A,α) =
JψK(A,α) =
Z
Σ-Struktur B = (B, J·KB ) mit B =
Jf KB (d) = −d, JRKB =≤
Belegung β(x) = 5, β(y ) = 3, β(z) = −1,
JϕK(B,β) =
JψK(B,β) =

Download Report