@@ -9,55 +9,55 @@ \subsection{Bisimulation}\label{bisimulation}
9
9
10
10
\begin {definition }{Bisimulation}
11
11
12
- Seien $ I_ {1}$ und $ I_ {2}$ Interpretationen. Relation
13
- $ \rho \subseteq \Delta ^{I_ {1}} \times \Delta ^{I_ {2}}$ ist Bisimulation
14
- zwischen $ I_ {1}$ und $ I_ {2}$ , wenn gilt:
12
+ Seien $ \MI _ {1}$ und $ \MI _ {2}$ Interpretationen. Relation
13
+ $ \rho \subseteq \Delta ^{\MI _ {1}} \times \Delta ^{\MI _ {2}}$ ist Bisimulation
14
+ zwischen $ \MI _ {1}$ und $ \MI _ {2}$ , wenn gilt:
15
15
16
16
\begin {enumerate }
17
17
\def\labelenumi {\arabic {enumi}.}
18
18
\item
19
19
Wenn $ d_{1}\text {\ $ \rho $ }\text {\ d}_{2}$ , dann gilt für alle
20
- Konzeptnamen A: $ d_{1} \in A^{I_ {1}}$ gdw. $ d_{2} \in A^{I_ {2}}$ .
20
+ Konzeptnamen A: $ d_{1} \in A^{\MI _ {1}}$ gdw. $ d_{2} \in A^{\MI _ {2}}$ .
21
21
\item
22
22
Wenn $ d_{1}\text {\ $ \rho $ }\text {\ d}_{2}$ und
23
- $ \left ( d_{1},d_{1}^{'} \right ) \in r^{I_ {1}}$ für beliebigen
24
- Rollennamen $ r$ , dann gibt es ein $ d_{2}^{'} \in \Delta ^{I_ {2}}$
23
+ $ \left ( d_{1},d_{1}^{'} \right ) \in r^{\MI _ {1}}$ für beliebigen
24
+ Rollennamen $ r$ , dann gibt es ein $ d_{2}^{'} \in \Delta ^{\MI _ {2}}$
25
25
mit $ {d'}_{1}\text {\ $ \rho $ }{\ d'}_{2}$ und
26
- $ \left ( d_{2},d_{2}^{'} \right ) \in r^{I_ {2}}$ .
26
+ $ \left ( d_{2},d_{2}^{'} \right ) \in r^{\MI _ {2}}$ .
27
27
\item
28
28
Wenn $ d_{1}\text {\ $ \rho $ }\text {\ d}_{2}$ und
29
- $ \left ( d_{2},d_{2}^{'} \right ) \in r^{I_ {2}}$ für beliebigen
30
- Rollennamen $ r$ , dann gibt es ein $ d_{1}^{'} \in \Delta ^{I_ {1}}$
29
+ $ \left ( d_{2},d_{2}^{'} \right ) \in r^{\MI _ {2}}$ für beliebigen
30
+ Rollennamen $ r$ , dann gibt es ein $ d_{1}^{'} \in \Delta ^{\MI _ {1}}$
31
31
mit $ {d'}_{1}\text {\ $ \rho $ }{\ d'}_{2}$ und
32
- $ \left ( d_{1},d_{1}^{'} \right ) \in r^{I_ {1}}$ .
32
+ $ \left ( d_{1},d_{1}^{'} \right ) \in r^{\MI _ {1}}$ .
33
33
\end {enumerate }
34
34
\end {definition }
35
35
36
- Seien $ I_ {1}$ und $ I_ {2}$ Interpretationen,
37
- $ d_{1} \in \Delta ^{I_ {1}}$ , $ d_{2} \in \Delta ^{I_ {2}}$ :
36
+ Seien $ \MI _ {1}$ und $ \MI _ {2}$ Interpretationen,
37
+ $ d_{1} \in \Delta ^{\MI _ {1}}$ , $ d_{2} \in \Delta ^{\MI _ {2}}$ :
38
38
39
- $ (I_ {1},d_{1}) \sim (I_ {2},d_{2})$ : Es gibt Bisimulation $ \rho $
40
- zwischen $ I_ {1}$ und $ I_ {2}$ mit $ d_{1}\text {\ $ \rho $ }\text {\ d}_{2}$ .
39
+ $ (\MI _ {1},d_{1}) \sim (\MI _ {2},d_{2})$ : Es gibt Bisimulation $ \rho $
40
+ zwischen $ \MI _ {1}$ und $ \MI _ {2}$ mit $ d_{1}\text {\ $ \rho $ }\text {\ d}_{2}$ .
41
41
Die leere Relation ist immer Bisimulation.
42
42
43
43
\begin {theorem }
44
- Seien $ I_ {1}$ , $ I_ {2}$ Interpretationen,
45
- $ d_{1} \in \Delta ^{I_ {1}}$ und $ d_{2} \in \Delta ^{I_ {2}}$ . Wenn
46
- $ (I_ {1},d_{1}) \sim (I_ {2},d_{2})$ , dann gilt für alle ALC-Konzepte
44
+ Seien $ \MI _ {1}$ , $ \MI _ {2}$ Interpretationen,
45
+ $ d_{1} \in \Delta ^{\MI _ {1}}$ und $ d_{2} \in \Delta ^{\MI _ {2}}$ . Wenn
46
+ $ (\MI _ {1},d_{1}) \sim (\MI _ {2},d_{2})$ , dann gilt für alle ALC-Konzepte
47
47
$ C$ :
48
48
49
- $$ d_{1} \in C^{I_ {1}}\ gdw.\ d_{2} \in C^{I_ {2}}$$
49
+ $$ d_{1} \in C^{\MI _ {1}}\ gdw.\ d_{2} \in C^{\MI _ {2}}$$
50
50
\end {theorem }
51
51
52
52
\textbf {T3.2. }
53
53
54
54
\begin {proof }
55
55
Beweisskizze per Induktion über die Struktur von C. Sei $ \rho $ eine
56
- Bisimulation zwischen $ I_ {1}$ und $ I_ {2}$ mit
56
+ Bisimulation zwischen $ \MI _ {1}$ und $ \MI _ {2}$ mit
57
57
$ d_{1}\text {\ $ \rho $ }\text {\ d}_{2}$ .
58
58
59
59
\textbf {I.A. } $ C = A$ ist Konzeptname. Nach Bedingung 1. der
60
- Bisimulation gilt $$ d_{1} \in A^{I_ {1}}\ gdw.\ d_{2} \in A^{I_ {2}}$$ .
60
+ Bisimulation gilt $$ d_{1} \in A^{\MI _ {1}}\ gdw.\ d_{2} \in A^{\MI _ {2}}$$ .
61
61
62
62
\textbf {I.S. } Unterscheide Fälle gemäß des äußersten Konstruktes von C.
63
63
Es genügen $ \neg $ ,$ \sqcap $ , $ \exists \text {r.C}$ :
@@ -71,7 +71,7 @@ \subsection{Bisimulation}\label{bisimulation}
71
71
\begin {quote }
72
72
\begin {equation }
73
73
\begin {split }
74
- d_{1} \in C^{I_ {1}} &\stackrel {Sem.}{gdw.} d_{1} \notin D^{\MI _{1}}\\
74
+ d_{1} \in C^{\MI _ {1}} &\stackrel {Sem.}{gdw.} d_{1} \notin D^{\MI _{1}}\\
75
75
&\stackrel {I.V.}{gdw.} d_{2} \notin D^{\MI _{2}} \\
76
76
&\stackrel {Sem.}{gdw.} d_{2} \in C^{\MI _{2}}
77
77
\end {split }
@@ -145,7 +145,7 @@ \subsubsection{Anwendungen von Bisimulation I}\label{theorem-3.4}
145
145
Beweisskizze. Finde Bisimulation für die dies nicht gilt.
146
146
147
147
\begin {proof }
148
- \textbf {$ \exists r.\top $ }
148
+ \textbf {$ \exists r^{-} .\top $ }
149
149
150
150
Betrachte 2 Interpretationen $ \MI $ und $ \MJ $
151
151
@@ -167,16 +167,16 @@ \subsubsection{Anwendungen von Bisimulation I}\label{theorem-3.4}
167
167
Man sieht, dass die Argumentation zum Beweis der Nicht-Ausdrückbarkeit immer auf dasselbe hinausläuft:
168
168
\begin {theorem }
169
169
170
- Sei $ E$ eine Eigenschaft. Wenn es Interpretation $ I_ {1}$ , $ I_ {2}$
171
- und Elemente $ d_{1} \in \Delta ^{I_ {1}}$ und
172
- $ d_{2} \in \Delta ^{I_ {2}}$ gibt, so dass
170
+ Sei $ E$ eine Eigenschaft. Wenn es Interpretation $ \MI _ {1}$ , $ \MI _ {2}$
171
+ und Elemente $ d_{1} \in \Delta ^{\MI _ {1}}$ und
172
+ $ d_{2} \in \Delta ^{\MI _ {2}}$ gibt, so dass
173
173
174
174
\begin {itemize }
175
175
\item
176
- $ \left ( I_ {1},d_{1} \right ) \in E$ und
177
- $ \left ( I_ {2},d_{2} \right ) \in E$ sowie
176
+ $ \left ( \MI _ {1},d_{1} \right ) \in E$ und
177
+ $ \left ( \MI _ {2},d_{2} \right ) \not \in E$ sowie
178
178
\item
179
- $ (I_ {1},d_{1}) \sim (I_ {2},d_{2})$
179
+ $ (\MI _ {1},d_{1}) \sim (\MI _ {2},d_{2})$
180
180
\end {itemize }
181
181
182
182
dann ist $ E$ nicht in $ \ALC $ ausdrückbar.
@@ -239,7 +239,7 @@ \subsubsection{Unravelling}\label{unravelling}
239
239
240
240
\begin {proof }
241
241
Mit Theorem genügt es folgende Bisimulation zu zeigen:
242
- $$ \left ( I ,end\left ( p \right ) \right )\sim \left ( J,p \right )$$ Definiere Relation: $$ \rho = \left \{ \left ( \text {end}\left ( p \right ),p \right ) \in \Delta ^{\MI } \times \Delta ^{\MJ }\ \right |\text {\ p\ }\mathrm {\text {ist}}\text {\ d}\mathrm {- Pfad}\}\ $$ (Bilde
242
+ $$ \left ( \MI ,end\left ( p \right ) \right )\sim \left ( J,p \right )$$ Definiere Relation: $$ \rho = \left \{ \left ( \text {end}\left ( p \right ),p \right ) \in \Delta ^{\MI } \times \Delta ^{\MJ }\ \right |\text {\ p\ }\mathrm {\text {ist}}\text {\ d}\mathrm {- Pfad}\}\ $$ (Bilde
243
243
alle Knoten in $ \MJ $ auf ihr Ende ab).
244
244
245
245
Zur Bisimulation:
@@ -325,7 +325,7 @@ \subsubsection{Größe von Konzepten und
325
325
326
326
\begin {itemize }
327
327
\item
328
- $ \sum _{C \sqsubseteq D \in T}^{}{ \left | C \right | + \left | D \right | + 1}$
328
+ $ \sum _{C \sqsubseteq D \in T}^{\left | C \right | + \left | D \right | + 1}$
329
329
\end {itemize }
330
330
\end {definition }
331
331
0 commit comments