-
Notifications
You must be signed in to change notification settings - Fork 0
/
x.html
137 lines (136 loc) · 38.2 KB
/
x.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
<!DOCTYPE html>
<html lang="de-DE">
<head>
<meta charset="utf-8" />
<meta name="generator" content="ublatt"/>
<title>0. Übungsblatt - Systeme hoher Sicherheit und Qualität - WiSe 20/21</title>
<style>
:root {
--sheet-num: '0';
--due-display: block;
}
</style>
<link rel="stylesheet" href="./dist/runtime/ublatt.css"/>
<link rel="stylesheet" href="./dist/runtime/modules/input.css"/>
</head>
<body>
<form class="ublatt">
<div class="head">
<span class="title">Systeme hoher Sicherheit und Qualität</span>
<span class="term">WiSe 20/21</span>
<ul class="lecturers">
<li>Martin Ring</li>
<li>Jil Tietjen</li>
</ul>
<span class="issued">11.11.2020</span>
<span class="due">18.11.2020</span>
</div>
<div class="main">
<section>
<h1>Aussagenlogik</h1>
<p>Gegeben sind folgende Elementaraussagen:</p>
<section><eqn><span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mtable rowspacing="0.15999999999999992em" columnalign="center left" columnspacing="1em"><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>C</mi><mo>:</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mtext>Es gibt Corona</mtext></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>K</mi><mo>:</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mtext>Es gibt eine Klimakatastrophe</mtext></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>P</mi><mo>:</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mtext>Wir haben ein Problem</mtext></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>Z</mi><mo>:</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mtext>Alle bleiben zuhause</mtext></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>A</mi><mo>:</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mtext>Alle halten Abstand</mtext></mstyle></mtd></mtr></mtable><annotation encoding="application/x-tex">
\begin{array}{cl}
C: & \text{Es gibt Corona}\\
K: & \text{Es gibt eine Klimakatastrophe}\\
P: & \text{Wir haben ein Problem}\\
Z: & \text{Alle bleiben zuhause}\\
A: & \text{Alle halten Abstand}
\end{array}
</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:6.000000000000001em;vertical-align:-2.7500000000000004em;"></span><span class="mord"><span class="mtable"><span class="arraycolsep" style="width:0.5em;"></span><span class="col-align-c"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:3.2500000000000004em;"><span style="top:-5.410000000000001em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.07153em;">C</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span></span></span><span style="top:-4.21em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.07153em;">K</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span></span></span><span style="top:-3.01em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span></span></span><span style="top:-1.8099999999999998em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.07153em;">Z</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span></span></span><span style="top:-0.6099999999999997em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span></span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:2.7500000000000004em;"><span></span></span></span></span></span><span class="arraycolsep" style="width:0.5em;"></span><span class="arraycolsep" style="width:0.5em;"></span><span class="col-align-l"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:3.2500000000000004em;"><span style="top:-5.410000000000001em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord text"><span class="mord">Es gibt Corona</span></span></span></span><span style="top:-4.21em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord text"><span class="mord">Es gibt eine Klimakatastrophe</span></span></span></span><span style="top:-3.01em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord text"><span class="mord">Wir haben ein Problem</span></span></span></span><span style="top:-1.8099999999999998em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord text"><span class="mord">Alle bleiben zuhause</span></span></span></span><span style="top:-0.6099999999999997em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord text"><span class="mord">Alle halten Abstand</span></span></span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:2.7500000000000004em;"><span></span></span></span></span></span><span class="arraycolsep" style="width:0.5em;"></span></span></span></span></span></span></span></eqn></section></math>
<p>Die nachfolgenden Sätze sollen als aussagenlogische Formeln ausgedrückt
werden. Geben sie jeweils auch die KNF an.</p>
<ol>
<li>
<p>Wenn es Corona und eine Klimakatastrophe gibt, haben wir ein Problem:</p>
<p><span class="input math"> </span></p>
<p>In KNF:</p>
<p><span class="input math"> </span></p>
</li>
<li>
<p>Wenn es Corona gibt, dann bleiben wir alle Zuhause:</p>
<p><span class="input math"> </span></p>
<p>In KNF:</p>
<p><span class="input math"> </span></p>
</li>
<li>
<p>Entweder es gibt Corona oder eine Klimakatastrophe.</p>
<p><span class="input math"> </span></p>
<p>In KNF:</p>
<p><span class="input math"> </span></p>
</li>
<li>
<p>Corona gibt es genau dann nicht, wenn alle Zuhause bleiben oder Abstand halten.</p>
<p><span class="input math"> </span></p>
<p>In KNF:</p>
<p><span class="input math"> </span></p>
</li>
</ol>
</section>
<section>
<h1>Prädikatenlogik</h1>
<div class="figure">
<p><img src="img/aufz%C3%BCge.jpg" alt="Die Aufzüge im MZH"></p>
</div>
<p>In dieser Aufgabe wird der Fahrstuhl im MZH betrachtet. Gegeben sind folgende
Prädikate:</p>
<section><eqn><span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mtable rowspacing="0.15999999999999992em" columnalign="left left" columnspacing="1em"><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi mathvariant="normal">fahrstuhl</mi><mo></mo><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>x</mi><mtext> ist ein Fahrstuhl</mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi mathvariant="normal">ebene</mi><mo></mo><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>y</mi><mtext> ist eine Ebene</mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi mathvariant="normal">neunteEbene</mi><mo></mo><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>z</mi><mtext> ist die neunte Ebene</mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi mathvariant="normal"><mi mathvariant="normal">t</mi><mover accent="true"><mi mathvariant="normal">u</mi><mo>¨</mo></mover><mi mathvariant="normal">r</mi><mi mathvariant="normal">A</mi><mi mathvariant="normal">u</mi><mi mathvariant="normal">f</mi></mi><mo></mo><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>x</mi><mrow><mtext> kann die T</mtext><mover accent="true"><mtext>u</mtext><mo>¨</mo></mover><mtext>r </mtext><mover accent="true"><mtext>o</mtext><mo>¨</mo></mover><mtext>ffnen</mtext></mrow></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi mathvariant="normal">istInEbene</mi><mo></mo><mo stretchy="false">(</mo><mi>x</mi><mo separator="true">,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>x</mi><mtext> ist in der Ebene y </mtext></mrow></mstyle></mtd></mtr></mtable><annotation encoding="application/x-tex">
\begin{array}{ll}
\operatorname{fahrstuhl}(x) & x \text{ ist ein Fahrstuhl}\\
\operatorname{ebene}(y) & y \text{ ist eine Ebene}\\
\operatorname{neunteEbene}(z) & z \text{ ist die neunte Ebene}\\
\operatorname{türAuf}(x) & x \text{ kann die Tür öffnen}\\
\operatorname{istInEbene}(x,y) & x \text{ ist in der Ebene y }
\end{array}
</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:6.000000000000001em;vertical-align:-2.7500000000000004em;"></span><span class="mord"><span class="mtable"><span class="arraycolsep" style="width:0.5em;"></span><span class="col-align-l"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:3.2500000000000004em;"><span style="top:-5.410000000000001em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mop"><span class="mord mathrm" style="margin-right:0.07778em;">f</span><span class="mord mathrm">a</span><span class="mord mathrm">h</span><span class="mord mathrm">r</span><span class="mord mathrm">s</span><span class="mord mathrm">t</span><span class="mord mathrm">u</span><span class="mord mathrm">h</span><span class="mord mathrm">l</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span></span></span><span style="top:-4.21em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mop"><span class="mord mathrm">e</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span></span></span><span style="top:-3.01em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mop"><span class="mord mathrm">n</span><span class="mord mathrm">e</span><span class="mord mathrm">u</span><span class="mord mathrm">n</span><span class="mord mathrm">t</span><span class="mord mathrm">e</span><span class="mord mathrm">E</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.04398em;">z</span><span class="mclose">)</span></span></span><span style="top:-1.8099999999999998em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mop"><span class="mord mathrm">t</span><span class="mord accent"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.66786em;"><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="mord mathrm">u</span></span><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="accent-body" style="left:-0.25em;"><span class="mord mathrm">¨</span></span></span></span></span></span></span><span class="mord mathrm">r</span><span class="mord mathrm">A</span><span class="mord mathrm">u</span><span class="mord mathrm" style="margin-right:0.07778em;">f</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span></span></span><span style="top:-0.6099999999999997em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mop"><span class="mord mathrm">i</span><span class="mord mathrm">s</span><span class="mord mathrm">t</span><span class="mord mathrm">I</span><span class="mord mathrm">n</span><span class="mord mathrm">E</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span></span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:2.7500000000000004em;"><span></span></span></span></span></span><span class="arraycolsep" style="width:0.5em;"></span><span class="arraycolsep" style="width:0.5em;"></span><span class="col-align-l"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:3.2500000000000004em;"><span style="top:-5.410000000000001em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal">x</span><span class="mord text"><span class="mord"> ist ein Fahrstuhl</span></span></span></span><span style="top:-4.21em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mord text"><span class="mord"> ist eine Ebene</span></span></span></span><span style="top:-3.01em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.04398em;">z</span><span class="mord text"><span class="mord"> ist die neunte Ebene</span></span></span></span><span style="top:-1.8099999999999998em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal">x</span><span class="mord text"><span class="mord"> kann die T</span><span class="mord accent"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.66786em;"><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="mord">u</span></span><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="accent-body" style="left:-0.25em;"><span class="mord">¨</span></span></span></span></span></span></span><span class="mord">r </span><span class="mord accent"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.66786em;"><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="mord">o</span></span><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="accent-body" style="left:-0.25em;"><span class="mord">¨</span></span></span></span></span></span></span><span class="mord">ffnen</span></span></span></span><span style="top:-0.6099999999999997em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord mathnormal">x</span><span class="mord text"><span class="mord"> ist in der Ebene y </span></span></span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:2.7500000000000004em;"><span></span></span></span></span></span><span class="arraycolsep" style="width:0.5em;"></span></span></span></span></span></span></span></eqn></section></math>
<p>Und folgende Funktion:</p>
<section><eqn><span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mtable rowspacing="0.15999999999999992em" columnalign="left left" columnspacing="1em"><mtr><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mi mathvariant="normal">anzahlPers</mi><mo></mo><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="false"><mrow><mtext>Gibt die Anzahl der Personen im Fahrstuhl zur</mtext><mover accent="true"><mtext>u</mtext><mo>¨</mo></mover><mtext>ck</mtext></mrow></mstyle></mtd></mtr></mtable><annotation encoding="application/x-tex">
\begin{array}{ll}
\operatorname{anzahlPers}(x) & \text{Gibt die Anzahl der Personen im Fahrstuhl zurück}
\end{array}
</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1.2000000000000002em;vertical-align:-0.35000000000000003em;"></span><span class="mord"><span class="mtable"><span class="arraycolsep" style="width:0.5em;"></span><span class="col-align-l"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.8500000000000001em;"><span style="top:-3.01em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mop"><span class="mord mathrm">a</span><span class="mord mathrm">n</span><span class="mord mathrm">z</span><span class="mord mathrm">a</span><span class="mord mathrm">h</span><span class="mord mathrm">l</span><span class="mord mathrm">P</span><span class="mord mathrm">e</span><span class="mord mathrm">r</span><span class="mord mathrm">s</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span></span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:0.35000000000000003em;"><span></span></span></span></span></span><span class="arraycolsep" style="width:0.5em;"></span><span class="arraycolsep" style="width:0.5em;"></span><span class="col-align-l"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.8500000000000001em;"><span style="top:-3.01em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord text"><span class="mord">Gibt die Anzahl der Personen im Fahrstuhl zur</span><span class="mord accent"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.66786em;"><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="mord">u</span></span><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="accent-body" style="left:-0.25em;"><span class="mord">¨</span></span></span></span></span></span></span><span class="mord">ck</span></span></span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:0.35000000000000003em;"><span></span></span></span></span></span><span class="arraycolsep" style="width:0.5em;"></span></span></span></span></span></span></span></eqn></section></math>
<p>Übersetzen Sie die folgenden Aussagen über den Fahrstuhl in Prädikatenlogik
erster Stufe bzw. in natürlichsprachliche Aussagen.</p>
<ol>
<li>
<p>Nichts ist ein Fahrstuhl und eine Ebene gleichzeitig.</p>
<p><span class="input math"> </span></p>
</li>
<li>
<p>In keinem Fahrstuhl sind mehr als acht Personen.</p>
<p><span class="input math"> </span></p>
</li>
<li>
<p>Jeder Fahrstuhl ist immer in genau einer Ebene.</p>
<p><span class="input math"> </span></p>
</li>
<li>
<p><eq><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi mathvariant="normal">∀</mi><mi>z</mi><mi mathvariant="normal">.</mi><mi mathvariant="normal">neunteEbene</mi><mo></mo><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>→</mo><mi mathvariant="normal">ebene</mi><mo></mo><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\forall z . \operatorname{neunteEbene}(z) \rightarrow \operatorname{ebene}(z)</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord">∀</span><span class="mord mathnormal" style="margin-right:0.04398em;">z</span><span class="mord">.</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mop"><span class="mord mathrm">n</span><span class="mord mathrm">e</span><span class="mord mathrm">u</span><span class="mord mathrm">n</span><span class="mord mathrm">t</span><span class="mord mathrm">e</span><span class="mord mathrm">E</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.04398em;">z</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">→</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mop"><span class="mord mathrm">e</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.04398em;">z</span><span class="mclose">)</span></span></span></span></eq></p>
<p><span class="input"> </span></p>
</li>
<li>
<p><eq><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi mathvariant="normal">∃</mi><mi>y</mi><mi mathvariant="normal">.</mi><mi mathvariant="normal">neunteEbene</mi><mo></mo><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><mi mathvariant="normal">∀</mi><mi>x</mi><mo separator="true">,</mo><mi>y</mi><mi mathvariant="normal">.</mi><mi mathvariant="normal">neunteEbene</mi><mo></mo><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∧</mo><mi mathvariant="normal">neunteEbene</mi><mo></mo><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>x</mi><mo>=</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\exists y . \operatorname{neunteEbene}(y) \wedge \forall x, y. \operatorname{neunteEbene}(x) \wedge \operatorname{neunteEbene}(y) \rightarrow (x=y)</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord">∃</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mord">.</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mop"><span class="mord mathrm">n</span><span class="mord mathrm">e</span><span class="mord mathrm">u</span><span class="mord mathrm">n</span><span class="mord mathrm">t</span><span class="mord mathrm">e</span><span class="mord mathrm">E</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">∧</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord">∀</span><span class="mord mathnormal">x</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mord">.</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mop"><span class="mord mathrm">n</span><span class="mord mathrm">e</span><span class="mord mathrm">u</span><span class="mord mathrm">n</span><span class="mord mathrm">t</span><span class="mord mathrm">e</span><span class="mord mathrm">E</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">∧</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mop"><span class="mord mathrm">n</span><span class="mord mathrm">e</span><span class="mord mathrm">u</span><span class="mord mathrm">n</span><span class="mord mathrm">t</span><span class="mord mathrm">e</span><span class="mord mathrm">E</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">→</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span></span></span></span></eq></p>
<p><span class="input"> </span></p>
</li>
<li>
<p><eq><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi mathvariant="normal">∀</mi><mi>x</mi><mi mathvariant="normal">.</mi><mi mathvariant="normal">fahrstuhl</mi><mo></mo><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∧</mo><mi mathvariant="normal">∃</mi><mi>y</mi><mi mathvariant="normal">.</mi><mi mathvariant="normal">neunteEbene</mi><mo></mo><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><mi mathvariant="normal">istInEbene</mi><mo></mo><mo stretchy="false">(</mo><mi>x</mi><mo separator="true">,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>→</mo><mi mathvariant="normal">¬</mi><mi mathvariant="normal"><mi mathvariant="normal">t</mi><mover accent="true"><mi mathvariant="normal">u</mi><mo>¨</mo></mover><mi mathvariant="normal">r</mi><mi mathvariant="normal">A</mi><mi mathvariant="normal">u</mi><mi mathvariant="normal">f</mi></mi><mo></mo><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\forall x . \operatorname{fahrstuhl}(x) \wedge \exists y . \operatorname{neunteEbene}(y) \wedge \operatorname{istInEbene}(x,y) \rightarrow \lnot \operatorname{türAuf}(x)</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord">∀</span><span class="mord mathnormal">x</span><span class="mord">.</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mop"><span class="mord mathrm" style="margin-right:0.07778em;">f</span><span class="mord mathrm">a</span><span class="mord mathrm">h</span><span class="mord mathrm">r</span><span class="mord mathrm">s</span><span class="mord mathrm">t</span><span class="mord mathrm">u</span><span class="mord mathrm">h</span><span class="mord mathrm">l</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">∧</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord">∃</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mord">.</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mop"><span class="mord mathrm">n</span><span class="mord mathrm">e</span><span class="mord mathrm">u</span><span class="mord mathrm">n</span><span class="mord mathrm">t</span><span class="mord mathrm">e</span><span class="mord mathrm">E</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">∧</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mop"><span class="mord mathrm">i</span><span class="mord mathrm">s</span><span class="mord mathrm">t</span><span class="mord mathrm">I</span><span class="mord mathrm">n</span><span class="mord mathrm">E</span><span class="mord mathrm">b</span><span class="mord mathrm">e</span><span class="mord mathrm">n</span><span class="mord mathrm">e</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">→</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord">¬</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mop"><span class="mord mathrm">t</span><span class="mord accent"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.66786em;"><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="mord mathrm">u</span></span><span style="top:-3em;"><span class="pstrut" style="height:3em;"></span><span class="accent-body" style="left:-0.25em;"><span class="mord mathrm">¨</span></span></span></span></span></span></span><span class="mord mathrm">r</span><span class="mord mathrm">A</span><span class="mord mathrm">u</span><span class="mord mathrm" style="margin-right:0.07778em;">f</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span></span></span></span></eq></p>
<p><span class="input"> </span></p>
</li>
</ol>
</section>
<section>
<h1>Zustandsautomaten</h1>
<p>Es gibt einen Fahrstuhl, der als Zustandsautomat modelliert werden soll. Der Fahrstuhl befindet sich zu Beginn im EG. Es gibt außerdem eine erste Etage und eine zweite Etage. In jeder Etage kann der Fahrstuhl die Tür öffnen. Der Zustandsautomat soll daher 6 Zustände haben. Es gibt für jede Etage Knöpfe, die gedrückt oder nicht gedrückt sind. Wenn die Etage ausgewählt wird, in der sich der Fahrstuhl gerade befindet, dann öffnet sich die Tür und schließt im nächsten Schritt wieder. Wenn nur Knöpfe von anderen Ebenen gedrückt sind, bewegt sich der Fahrstuhl eine Ebene in deren Richtung. Wenn in der ersten Ebene sowohl der Knopf für die 2. Etage und das EG gedrückt sind, kann sich der Fahrstuhl nichtdeterministisch für eine entscheiden. Ist keiner der Knöpfe gedrückt, dann passiert nichts.</p>
<div class="info">
<p>Der Zustandsautomat wird in <a href="https://mermaid-js.github.io/mermaid/#/stateDiagram">Mermaid Syntax</a> eingegeben.</p>
</div>
<pre class="input mermaid"><code>stateDiagram-v2
E0
</code></pre></section>
</div>
</form>
<script type="module">
import Ublatt from './dist/runtime/ublatt.js'; import Input from './dist/runtime/modules/input.js'; import Math from './dist/runtime/modules/input/math.js'; import Mermaid from './dist/runtime/modules/input/mermaid.js';const meta = {"lang":"de-DE","title":"Systeme hoher Sicherheit und Qualität","subtitle":"WiSe 20/21","author":["Dieter Hutter","Jil Tietjen","Martin Ring"],"sheet":0,"date":"11.11.2020","due":"18.11.2020"}; const ublatt = new Ublatt(document.querySelector('form.ublatt'),meta); window.ublatt = ublatt; const input = new Input(); ublatt.registerModule('input',input); const math = new Math(); input.registerModule('math',math); const mermaid = new Mermaid(); input.registerModule('mermaid',mermaid); ublatt.init({"course":"Systeme hoher Sicherheit und Qualität","sheet":"0","authors":[{"name":"Martin Ring","matriculation_number":"123456","email":"martin.ring@dfki.de"},{"name":"Jil Tietjen","matriculation_number":"654431","email":"jil.tietjen@dfki.de"}],"solutions":{"e1":"C \\land K \\rightarrow P","e1_2":"\\begin{array}{c|c|c|c}\nC & K & P & C \\land K \\rightarrow P\\\\\\hline\n0 & 0 & 0 & 1\\\\\n0 & 0 & 1 & 1\\\\\n0 & 1 & 0 & 1\\\\\n0 & 1 & 1 & 1\\\\\n1 & 0 & 0 & 1\\\\\n1 & 0 & 1 & 1\\\\\n1 & 1 & 0 & 0\\\\\n1 & 1 & 1 & 1\\\\\n\\end{array}\n\n\\Longrightarrow \n\n\\begin{array}{}\n\\\\\n\\\\\n\\\\\n\\\\\n\\\\\n\\\\\n(\\lnot C \\lor \\lnot K \\lor P)\\\\\n\\end{array}","e1_3":"C \\rightarrow Z","e1_4":"\\begin{array}{c|c|c}\nC & Z & C \\rightarrow Z\\\\\\hline\n0 & 0 & 1\\\\\n0 & 1 & 1\\\\\n1 & 0 & 0\\\\\n1 & 1 & 1\\\\\n\\end{array}\n\n\\Longrightarrow\n\n\\begin{array}{}\n\\\\\n\\\\\n(\\lnot C \\lor Z)\n\\\\\n\\end{array}","e1_5":"(C \\land \\lnot K) \\lor (\\lnot C \\land K)","e1_6":"\\begin{array}{c|c|c}\nC & K & (C \\land \\lnot K) \\lor (\\lnot C \\land K)\\\\\\hline\n0 & 0 & 0\\\\\n0 & 1 & 1\\\\\n1 & 0 & 1\\\\\n1 & 1 & 0\\\\\n\\end{array}\n\n\\Longrightarrow\n\n\\begin{array}{l}\n\\\\\n(C \\lor K) & \\land \\\\\n\\\\\n\\\\\n(\\lnot C \\lor \\lnot K)\n\\end{array}","e1_7":"\\lnot C \\leftrightarrow Z \\lor K","e1_8":"\\begin{array}{c|c|c|c}\nC & Z & K & \\lnot C \\leftrightarrow Z \\lor K\\\\\\hline\n0 & 0 & 0 & 0\\\\\n0 & 0 & 1 & 1\\\\\n0 & 1 & 0 & 1\\\\\n0 & 1 & 1 & 1\\\\\n1 & 0 & 0 & 1\\\\\n1 & 0 & 1 & 0\\\\\n1 & 1 & 0 & 0\\\\\n1 & 1 & 1 & 0\\\\\n\\end{array}\n\n\\Longrightarrow\n\n\\begin{array}{l}\n\\\\\n(C \\lor Z \\lor K) &\\land\\\\\n\\\\\n\\\\\n\\\\\n\\\\\n(\\lnot C \\lor Z \\lor K) & \\land\\\\\n(\\lnot C \\lor \\lnot Z \\lor K) &\\land\\\\\n(\\lnot C \\lor \\lnot Z \\lor \\lnot K)\n\\end{array}","e2":"\\nexists x. \\operatorname{fahrstuhl}(x) \\land \\operatorname{ebene}(x)","e2_2":"\\forall x. \\operatorname{fahrstuhl}(x) \\rightarrow \\operatorname{anzahlPers}(x) \\le 8","e2_3":"\\forall x. \\operatorname{fahrstuhl}(x) \\rightarrow (\\exists x. \\operatorname{ebene}(y) \\land \\operatorname{istInEbene}(x,y)) \\land \\forall y,z.\\operatorname{istInEbene}(x,y) \\land \\operatorname{istInEbene}(x,z) \\rightarrow y = z","e2_4":"Jede neunte Ebene ist eine Ebene","e2_5":"Es gibt genau eine neunte Ebene","e2_6":"Kein Fahrstuhl in der neunten Ebene kann die Tür öffnen","e3":"stateDiagram-v2\n [*] --> E0\n E0 --> E0 : 000\n E0 --> E0_Offen : 0??\n E0_Offen --> E0\n E0 --> E1 : 010, 001, 011\n E1 --> E0 : 1??\n E1 --> E1 : 000\n E1 --> E1_Offen : ?1?\n E1_Offen --> E1 : ?0?\n E1 --> E2 : ?01\n E2 --> E1 : 100, 110, 010\n E2 --> E2 : ∅\n E2 --> E2_Offen : ??1\n E2_Offen --> E2 : ??0"}}, {"course":"Systeme hoher Sicherheit und Qualität","sheet":"0","authors":[{"name":"Martin Ring","matriculation_number":"123456","email":"martin.ring@dfki.de"},{"name":"Jil Tietjen","matriculation_number":"654431","email":"jil.tietjen@dfki.de"}],"solutions":{"e1":"C \\land K \\rightarrow P","e1_2":"\\begin{array}{c|c|c|c}\nC & K & P & C \\land K \\rightarrow P\\\\\\hline\n0 & 0 & 0 & 1\\\\\n0 & 0 & 1 & 1\\\\\n0 & 1 & 0 & 1\\\\\n0 & 1 & 1 & 1\\\\\n1 & 0 & 0 & 1\\\\\n1 & 0 & 1 & 1\\\\\n1 & 1 & 0 & 0\\\\\n1 & 1 & 1 & 1\\\\\n\\end{array}\n\n\\Longrightarrow \n\n\\begin{array}{}\n\\\\\n\\\\\n\\\\\n\\\\\n\\\\\n\\\\\n(\\lnot C \\lor \\lnot K \\lor P)\\\\\n\\end{array}","e1_3":"C \\rightarrow Z","e1_4":"\\begin{array}{c|c|c}\nC & Z & C \\rightarrow Z\\\\\\hline\n0 & 0 & 1\\\\\n0 & 1 & 1\\\\\n1 & 0 & 0\\\\\n1 & 1 & 1\\\\\n\\end{array}\n\n\\Longrightarrow\n\n\\begin{array}{}\n\\\\\n\\\\\n(\\lnot C \\lor Z)\n\\\\\n\\end{array}","e1_5":"(C \\land \\lnot K) \\lor (\\lnot C \\land K)","e1_6":"\\begin{array}{c|c|c}\nC & K & (C \\land \\lnot K) \\lor (\\lnot C \\land K)\\\\\\hline\n0 & 0 & 0\\\\\n0 & 1 & 1\\\\\n1 & 0 & 1\\\\\n1 & 1 & 0\\\\\n\\end{array}\n\n\\Longrightarrow\n\n\\begin{array}{l}\n\\\\\n(C \\lor K) & \\land \\\\\n\\\\\n\\\\\n(\\lnot C \\lor \\lnot K)\n\\end{array}","e1_7":"\\lnot C \\leftrightarrow Z \\lor K","e1_8":"\\begin{array}{c|c|c|c}\nC & Z & K & \\lnot C \\leftrightarrow Z \\lor K\\\\\\hline\n0 & 0 & 0 & 0\\\\\n0 & 0 & 1 & 1\\\\\n0 & 1 & 0 & 1\\\\\n0 & 1 & 1 & 1\\\\\n1 & 0 & 0 & 1\\\\\n1 & 0 & 1 & 0\\\\\n1 & 1 & 0 & 0\\\\\n1 & 1 & 1 & 0\\\\\n\\end{array}\n\n\\Longrightarrow\n\n\\begin{array}{l}\n\\\\\n(C \\lor Z \\lor K) &\\land\\\\\n\\\\\n\\\\\n\\\\\n\\\\\n(\\lnot C \\lor Z \\lor K) & \\land\\\\\n(\\lnot C \\lor \\lnot Z \\lor K) &\\land\\\\\n(\\lnot C \\lor \\lnot Z \\lor \\lnot K)\n\\end{array}","e2":"\\nexists x. \\operatorname{fahrstuhl}(x) \\land \\operatorname{ebene}(x)","e2_2":"\\forall x. \\operatorname{fahrstuhl}(x) \\rightarrow \\operatorname{anzahlPers}(x) \\le 8","e2_3":"\\forall x. \\operatorname{fahrstuhl}(x) \\rightarrow (\\exists x. \\operatorname{ebene}(y) \\land \\operatorname{istInEbene}(x,y)) \\land \\forall y,z.\\operatorname{istInEbene}(x,y) \\land \\operatorname{istInEbene}(x,z) \\rightarrow y = z","e2_4":"Jede neunte Ebene ist eine Ebene","e2_5":"Es gibt genau eine neunte Ebene","e2_6":"Kein Fahrstuhl in der neunten Ebene kann die Tür öffnen","e3":"stateDiagram-v2\n [*] --> E0\n E0 --> E0 : 000\n E0 --> E0_Offen : 0??\n E0_Offen --> E0\n E0 --> E1 : 010, 001, 011\n E1 --> E0 : 1??\n E1 --> E1 : 000\n E1 --> E1_Offen : ?1?\n E1_Offen --> E1 : ?0?\n E1 --> E2 : ?01\n E2 --> E1 : 100, 110, 010\n E2 --> E2 : ∅\n E2 --> E2_Offen : ??1\n E2_Offen --> E2 : ??0"}})
</script>
</body>
</html>