Database Reference
In-Depth Information
Definition 3.44 (Variablenbelegung)
Sei I = U
I
,
Func
I
,
Pred
I
)eineΣ-
Interpretation und V eine Menge von Variablen. Eine
Variablenbelegung
(engl.
va-
riable assignment
) ist eine Funktion α : V
→
U
I
.
Definition 3.45 (Termauswertung)
Gegeben sei ein Term t
∈
Term
Σ
(V ), eine
Σ-Interpretation I und eine Variablenbelegung α : V
U
I
.Die
Termauswertung
von
t
in
I
unter
α (oder:
Wert von
t
in
I
unter
α), geschrieben [[t]]
I,α
, ist gegeben
durch eine Funktion
→
[[ ]]
I,α
: Term
Σ
(V )
→
U
I
und ist definiert durch
[[ x]]
I,α
=
α(x)
[[ f (t
1
,...,t
n
)]]
I,α
=
f
I
([[t
1
]]
I,α
,...,[[ t
n
]]
I,α
)
wobei x eine Variable und f ein n-stelliges (n
≥
0) Funktionssymbol ist.
So wird der Term
Max
in der Interpretation I
1
aus Beispiel 3.41 zu
ich
und in der
Interpretation I
2
zu
mein Lieblingsopa
ausgewertet.
Selbsttestaufgabe 3.46 (Termauswertung in PL1)
Welches Element des
Universums liefert jeweils der Term
nf(nf(b))
in den beiden Interpretationen aus
der Selbsttestaufgabe 3.42?
3.5.3
Formeln und Formelauswertung
Definition 3.47 (atomare Formel, Atom)
Eine
atomare Formel
(oder
Atom
)
uber einer Signatur Σ = (
Func
,
Pred
) und einer Menge V von Variablen wird wie
folgt gebildet:
(1)
p
falls p ∈
Pred
und p hat die Stelligkeit 0
(2)
p(t
1
,...,t
n
)
falls p
Pred
mit der Stelligkeit n>0
und t
1
,...,t
n
∈
∈
Term
Σ
(V )
Mit Hilfe der Termauswertung konnen wir nun auch jeder atomaren Formel einen
Wahrheitswert zuweisen.
Definition 3.48 (Wahrheitswert atomarer Formeln unter
α
)
In einer Inter-
pretation I ist der Wahrheitswert einer atomaren Formel p(t
1
,...,t
n
) unter einer
Variablenbelegung α
true
genau dann, wenn die Auswertung der Terme t
1
,...,t
n
in I unter α ein Tupel von Elementen des Universums liefert, das in der Relation
p
I
,diep in I zugeordnet wird, enthalten ist:
[[ p(t
1
,...,t
n
)]]
I,α
=
true
gdw. ([[t
1
]]
I,α
,...,[[ t
n
]]
I,α
)
∈
p
I
So wird die atomare Formel
Großvater(Max, Moritz)
in der Interpretation I
1
aus
Beispiel 3.41 zu
true
und in der Interpretation I
2
zu
false
ausgewertet.
