====== AP4, IN4 Výroková logika ======

===== Zadání =====
IN(syntax, sémantika, odvozovací systém výrokové logiky, důkazy ve výrokové logice, pravdivost a dokazatelnost logických formulí)

AP(syntax, sémantika, odvozovací systém výrokové logiky, důkazy ve výrokové logice, pravdivost a dokazatelnost logických formulí, rezoluce)

===== Vypracování =====
=== Logika ===
**Logika** se zabývá problematikou správnosti usuzování (vztah vyplývání). Na usuzování však logiku zajímají pouze vybrané aspekty. **Usuzování** chápeme jako určitý myšlenkový proces. Psychologické aspekty tohoto procesu však logika zcela opomíjí, stejně jako jeho obsahovou stránku. Zabývá se především analýzou formální stavby úsudků jako základních jednotek usuzování. **Úsudkem rozumíme** takový myšlenkový postup, kterým dospíváme od nějakých tvrzení, která nazýváme **předpoklady** (premisy), k jinému tvrzení, které nazýváme **závěr** (důsledek). Při studiu úsudků logiku zajímá pouze jejich **forma, nikoliv konkrétní obsah**. Proto úsudkem je z hlediska logiky schéma tvaru:

//A<sub>1</sub>, A<sub>2</sub>, …, A<sub>n</sub> / B,//

kde výrazy A<sub>1</sub>, A<sub>2</sub>, …, A<sub>n</sub> reprezentují nějaká tvrzení a výraz B tvrzení, které je závěrem. Je-li úsudek daného tvaru platný (z pravdivých premis vždy získáme pravdivý závěr), říkáme, že závěr B vyplývá z premis A<sub>1</sub>, A<sub>2</sub>, …, A<sub>n</sub> (A<sub>1</sub>, A<sub>2</sub>, …, A<sub>n</sub>  implikuje B [2]).[1]

Logika je schopna (svými prostředky) kontrolovat správnost pouze u deduktivních úsudků. Porovnejte následující dva úsudky:
<box>

všichni lidé jsou smrtelní, Sokrates je člověk;
tudíž Sokrates je smrtelný

a

slunce doposud vyšlo každý den;
tudíž (asi) vyjde i zítra.[1]
</box>

První z nich je běžný příklad deduktivního úsudku, který je považován za platný. Druhý úsudek je považován za deduktivně neplatný — je to pravděpodobnostní úsudek.
Rozdíl mezi deduktivními a pravděpodobnostními úsudky je mj. v tom, že u platného deduktivního úsudku je pravdivost závěru zaručena pravdivostí premis, kdežto u pravděpodobnostního úsudku pravdivost premis nezaručuje jistou pravdivost závěru, pouze jeho pravděpodobnost (v uvedeném úsudku je tato pravděpodobnost jistě vysoká). [1]

**Logika** poskytuje nástroj pro budování (vědeckých) teorií (teorie grup, modální logiky). Například výpočtová logika umožňuje automatizaci důkazů a programování v jazyce Prolog (logické programování). [2]

=== Klasifikace logik ===
Nejobecnější klasifikací usuzování vůbec je rozdělení na:
  * **Mentální** (neformální) – usuzování všeobecně („selský rozum”), to co je poznatelné
  * **Formální** – to co je poznané a definované, metody odvozování.
    * Rozlišujeme **dvouhodnotovou** a **vícehodnotovou logiku** podle toho, zda připouštíme k ohodnocení tvrzení právě dvě pravdivostní hodnoty, tj. „pravda“ a “nepravda“, nebo více než dvě pravdivostní hodnoty.
    * Dále rozlišujeme logiku **extenzionální** a **intensionální** především podle toho, jakých spojek se užívá pro vytvoření složených tvrzení. U extenzionální pravdivost formule závisí jen na pravdivosti jejich složek („ne“, „a“, „nebo“), naopak u intensionální („možná“, „věřím“…).
    * Logika, která je **dvouhodnotová a extenzionální se nazývá klasická logika**. Dělí se dále podle detailnosti analýzy na **logiku výrokovou a predikátovou**.

==Klasická logika==

  * **Výroková logika**
  "Nebude-li pršet nezmoknem"  <math>(p \wedge \neg q \Rightarrow r)</math>. Více viz. níže.
  * **Predikátová logika**
    * 1. řádu: "Není pravda, že všichni lidé jsou spokojení." <math>\neg\forall x: (clovek(x) \Rightarrow spokojeny(x))</math>
    * 2. řádu: "Existuje vlastnost, kterou mají všichni lidé." <math>\exists P \forall x: (clovek(x) \Rightarrow P(x))</math>
[1] a [2]

=== Metajazyk ===
Žádný jazyk nelze systematicky vybudovat pouze pomocí jeho vlastních výrazových prostředků. K tomuto účelu vždy potřebujeme další jazyk (vyšší expresivní úrovně), v němž pak také můžeme formulovat výpovědi o výrazech toho nového jazyka. Jazyk který budujeme, nazveme **objektový jazyk** a jazyk, ve kterém hovoříme o objektovém jazyce, nazveme **metajazyk**. Nerozlišování objektového jazyka a metajazyka vede ke vzniku tzv. sémantických paradoxů. Např. paradox lháře: "Tato věta je nepravdivá".[1]

=== Výroková logika ===
<note important>Výroková logika je teorií logických spojek chápaných jako pravdivostní funkce. [1] Zabývá se způsoby tvoření výroků pomocí spojek a vztahy mezi pravdivostí různých výroků. [2]</note>

Nezabývá se smyslem výroků, jelikož má extenzionální charakter. Výroková logika zkoumá uvedené jevy prostřednictvím umělého jazyka používajícího **výrokových symbolů, logických spojek a závorek**. Jelikož sémantika tohoto jazyka je extenzionální, lze si představit, že výroková logika uznává pouze dva výroky: jeden, který reprezentuje všechny pravdivé výroky a druhý, který reprezentuje ty nepravdivé. [1]

==== Syntax ====
Výroková logika rozlišuje na syntaktické úrovni dva typy výroků — jednoduché (elementální) a složené:

<note important>**Výrok** je tvrzení nebo jazykový výraz, o jehož (ne)pravdivosti lze uvažovat.[1]
**Jednoduchý výrok** je výrok, který neobsahuje žádnou logickou spojku.
**Složený výrok** je výrok, který obsahuje alespoň jednu logickou spojku.[2]</note>

<box |Příklady:>**Výroky**:
  * je pět hodin
  * 2 + 3 = 5
  * pokud nenapíšeš úkoly a neuklidíš, nepůjdeme do kina
**Výrazy, které nejsou výroky**:
  * Kolik je hodin?
  * 2 + 3
  * napiš úkoly a ukliď
</box| [2]>

===Pravdivostní spojky (funkce)===
<note important>
Pravdivostní hodnota složeného výroku je jednoznačně určena pravdivostními hodnotami složek. **Uvažujeme-li n-ární spojku, pak tato spojka je funkcí, která přiřazuje n-tici pravdivostních hodnot určitou pravdivostní hodnotu.** Počet pravdivostních hodnot je konečný, jsou dvě (pravda, nepravda).[1]</note>

Každou n-ární spojku (jako pravdivostní funkci) lze zadat tabulkou o 2<sup>n</sup> řádcích, tzv. **pravdivostní tabulkou**.[1]

Počet vzájemně různých n-árních spojek je <math> 2^{2^n} </math>[1]. 

==Nulární výrokové spojky==
<note important>Nulární pravdivostní funkce (nezávisí na žádném argumentu) jsou konstanty odpovídající pravdivostním hodnotám 0,1. [2]</note>
==Unární (jednoargumentové) výrokové spojky==
^ p ^ ^ F<sub>1</sub> ^ F<sub>2</sub> ^ F<sub>3</sub> ^ F<sub>4</sub> ^
| 1 | | 1 | 1 | 0 | 0 |
| 0 | | 1 | 0 | 1 | 0 |

**F<sub>1</sub>**: unární verum,
**F<sub>2</sub>**: unární projekce p,
**F<sub>3</sub>**: negace p (ozn. ¬p);jediná netriviální unární funkce,
**F<sub>4</sub>**: unární falsum.
[1],[2]

==Binární výrokové spojky==
Přehled nejpoužívanějších spojek:
^ p ^ q ^ ^ <math>\vee</math> ^ <math>\wedge</math> ^ <math>\Rightarrow</math> ^ <math>\Leftrightarrow</math> ^ F<sub>5</sub> ^ F<sub>6</sub> ^ F<sub>7</sub> ^
| 1 | 1 | | 1 | 1 | 1 | 1 | 0 | 0 | 0 |
| 1 | 0 | | 1 | 0 | 0 | 0 | 1 | 1 | 0 |
| 0 | 1 | | 1 | 0 | 1 | 0 | 1 | 1 | 0 |
| 0 | 0 | | 0 | 0 | 1 | 1 | 1 | 0 | 1 |

<math>\vee</math> — **disjunkce** (alternativa; a nebo; OR)
<math>\wedge</math> — **konjunkce** (a zároveň; AND)
<math>\Rightarrow</math> — **implikace** (jestliže p, pak q; předpoklad <math>\Rightarrow</math> důsledek)
<math>\Leftrightarrow</math> — **ekvivalence** (právě tehdy,když;iff - if and only if)
**F<sub>5</sub>** — **Shefferova funkce** (negace konjunkce;NAND;"... je neslučitelné s ...")
**F<sub>6</sub>** — **nonekvivalence** (spojka nebo ve vylučovacím smyslu;"buď ...,anebo ...";XOR - eXclusive OR)
**F<sub>7</sub>** — **Nicodova (Peirceova) funkce** (negace disjunkce;NOR;"ani ..., ani ...")


<note>
  * Spojky <math>\vee , \wedge</math> jsou komutativní (hodnota funkce nezávisí na pořadí argumentů).
  * Běžně se používá infixový zápis <math>(p \vee q)</math>.
  * <math>\Leftrightarrow</math> je komutativní, <math>\Rightarrow</math> není komutativní.
</note>
[1],[2]


==Symbolický jazyk výrokové logiky==
<note important>
**Jazyk výrokové logiky má tuto abecedu a gramatiku**:
  * **Abeceda**:
    - Výrokové symboly: p, q, r, s ,případně p<sub>1</sub>, p<sub>2</sub>, ...
    - Symboly pro spojky: <math>\neg , \vee , \wedge , \Rightarrow , \Leftrightarrow</math>
    - pomocné symboly: (, ), [, ], {, }
  * **Gramatika** sestává z pravidel:
    - každý výrokový symbol je správně utvořenou formulí výrokové logiky (ve zkratce s. u. f. VL) — tzv. atomická formule;
    - je-li výraz //A// s. u. f. VL, pak výraz ¬(//A//) je s. u. f. VL;
    - jsou-li výrazy //A// a //B// s. u. f. VL, pak také výrazy (//A//) <math>\vee</math> (//B//), (//A//) <math>\wedge</math> (//B//), (//A//) <math>\Rightarrow</math> (//B//), (//A//) <math>\Leftrightarrow</math> (//B//) jsou s. u. f. VL;
    - jen výrazy utvořené podle 1,2,3 jsou s. u. f. VL.
[1]
</note>
<note>Symboly //A// a //B// z bodů 2 a 3 této induktivní definice jsou výrazy metajazyka. Nepatří tedy do jazyka výrokové logiky, ale označují jeho libovolné výrazy (správně utvořené formule). Závorky lze vynechat, pokud odstraněním nedojde k nejednoznačnostem.[1]</note>

==Reprezentace výroků v přirozeném jazyce==
Věta:"Pokud rychle napíšeš úkoly a venku bude hezky, půjdeme na procházku nebo pojedeme na koupaliště."

p — "rychle napíšeš úkoly"
r — "venku bude hezky"
s — "půjdeme na procházku"
t — "pojedeme na koupaliště"

Výsledná reprezentace v symbolickém jazyce je: <math>(p \wedge r)\Rightarrow(s \vee t)</math>

<note warning>Převod z přirozeného jazyka do symbolického jazyka výrokové logiky nemusí být vždy jednoznačný.</note>

[2]

==== Sémantika ====
<note important>**Pravdivostní ohodnocení** (interpretace) je funkce přiřazující všem atomickým formulím dané úvahy pravdivostní hodnoty (tj. každému výrokovému symbolu přiřadí 0 nebo 1).
**Valuace** je rozšíření interpretace z atomických na všechny formule dle tabulky pro výrokové spojky.

Interpretace //I// splňuje formuli //A// (formule je pravdivá v //I//, resp. odpovídající valuace //I'(A)// = 1), pokud
  - //A// je výrokový symbol a //I(A)// = 1
  - //A// je <math>\neg B</math> a //I// nesplňuje //B//, resp. //I'(B)// = 0
  - //A// je tvaru <math>B \wedge C</math> a //I// splňuje //B// i //C//, resp. //I'(B) = I'(C)// = 1
  - //A// je tvaru <math>B \vee C</math> a //I// splňuje //B// nebo //C//, resp. //I'(B)// = 1 nebo //I'(C)// = 1
  - //A// je tvaru <math>B \Rightarrow C</math> a //I// nesplňuje //B// nebo splňuje //C//, resp. //I'(B)// = 0 nebo //I'(C)// = 1
  - //A// je tvaru <math>B \Leftrightarrow C</math> a //I// splňuje //B// i //C// nebo //I// nesplňuje //B// i //C//, resp. //I'(B)// = //I'(C)//
[2]</note>

<note important>Formule A se nazývá **tautologie**, je-li splňována každou interpretací. Např.<math>\neg p \vee p</math>
Formule A se nazývá **kontradikce**, jestliže není splňována žádnou interpretací. Např.<math>\neg p \wedge p</math>
Říkáme, že **formule //A// je splnitelná**, je-li splňována aspoň jednou interpretací //I//, kterou pak nazýváme **model formule** //A//.
Množina formulí T je **splnitelná**, jestliže existuje ohodnocení //I// takové, že každá formule //A// ∈ T je splňována //I//. Tuto interpretaci pak nazýváme **model množiny** T.
Říkáme, že formule //A// **logicky vyplývá (na základě výrokové logiky)** z množiny T a tuto skutečnost označíme <math>T \vdash A</math> (případně T ∴ A), jestliže pro každý model //I// množiny T je formule //A// interpretací //I// splňována.</note>
<note>Tautologií je nekonečně mnoho.[2]</note>
Ke zjištění pravdivosti formulí pro všechny možné interpretace používáme **tabulkovou metodu**.
{{:home:inf:tabulkovametoda.jpg|}}[2]
**Zásady**:
Vyhodnocení probíhá po složkách (podformulích) dané formule (výrok. symboly, negace, ..., celá formule).
Zápis pravdivostní hodnoty provedeme v řádku s příslušnou interpretací pod vyhodnocovanou spojkou (výr. symbol).[2]


==== Odvozovací systém výrokové logiky ====
===Formální systém výrokové logiky===
Na rozdíl od vyhodnocování (interpretace, resp. valuace) logických formulí na základě atomických formulí (výrokových symbolů) klademe na formální systém výr. logiky požadavek na **dokazování výr. formulí**. Tj. **zjištění, zda-li pravdivost dané formule vyplývá z pravdivostí jiných formulí**. 

<note important>**Formálním systémem výrokové logiky** se rozumí **jazyk** výrokové logiky a **deduktivní soustava**, která je tvořena odvozovacími pravidly a případně axiomy. Za **axiomy** (výchozí tvrzení přijímaná bez důkazu) volíme vhodná schémata tautologií, **odvozovací pravidlo** chápeme jako operace na formulích umožňující konstrukce důkazů a stačí jediné - pravidlo **modus ponens**. Po tomto pravidle požadujeme korektnost, to znamená, aby z pravdivých premis byl odvozen pravdivý závěr.
Formální systémy jsou postaveny výhradně na syntaktické bázi, jazyk logiky neinterpretujeme, provádíme s ním pouze syntaktické manipulace — důkazy.[2]


**Formální systémy lze rozdělit na**:
  - axiomatické (méně pravidel)
  - předpokladové (méně axiomů) — např. Gentzenovský systém (kalkul sekventů), jediný axiom (<math>A \vdash A</math>). Důkaz sekventu je strom, v jehož kořeni je dokazovaný sekvent, v listech axiomy a každý uzel (závěr) se svými přímými následovníky (předpoklady) představuje instanci některého z pravidel systému.

**Požadované vlastnosti formálních systémů**:
  * **korektnost (bezespornost)**: je dána výběrem axiomů a odvozovacích pravidel; systém je korektní, nelze-li v něm zároveň odvodit tvrzení i jeho negaci. Ve sporném systému lze odvodit cokoliv. **Vyžadována vždy.**
  * **úplnost**: připojením neodvoditelné věty k úplnému systému se tento stane sporným. Nevyžadována vždy – úplné jsou pouze velmi jednoduché teorie.
  * **rozhodnutelnost**: existence algoritmu pro ověření dokazatelnosti libovolné formule. V axiom. systémech podmíněna úplností; zpravidla splněna pouze pro určité třídy formulí.
  * **nezávislost axiomů**: nezávislý axiom nelze odvodit z ostatních axiomů;závislý axiom může být vypuštěn z dané soustavy axiomů.
[1] a [2] 
</note>

==Modus ponens (MP)==
MP je základní a nejdůležitější odvozovací pravidlo. Jeho tvar:
<math>\frac{A, \quad A \Rightarrow B}B</math>
MP říká, že když máme formule A a A ⇒ B pak z toho vyplývá platnost B.

==== Důkazy ve výrokové logice ====
<note important>**Důkaz** je v daném systému konečná posloupnost správně utvořených formulí (kroků důkazu), z nichž každá je buď axiómem nebo byla odvozena aplikací některého pravidla odvození na některé předcházející správně utvořené formule.
Určitá **formule je dokazatelná** v daném systému tehdy a jen tehdy, když v tomto systému existuje důkaz, jehož je tato formule členem. (<math>\vdash</math>).
**Teorém** je v systému S formule, která je dokazatelná v systému S.[3]</note>

==== Pravdivost a dokazatelnost logických formulí ====
<note important>
  * **Pravdivost** logické formule je dána sémantikou této formule. Kdežto, 
  * **dokazatelnost** (odvoditelnost) logické formule je posuzována syntaxí. Říkáme, že formule je dokazatelná, pokud k této formuli existuje důkaz. Těchto důkazů je nekonečně mnoho.
</note>


==== Rezoluce ====
<note important>Rezoluce je **formální systém** výrokové logiky vhodný pro **strojové dokazování** (Prolog) a je založena na vyvracení — dokazuje se nesplnitelnost formulí. 
Rezoluce pracuje s formulemi v KNF((Konjunktivní Normální Forma)), notace je však jiná:
  * **klauzule** je konečná množina literálů (chápána jako jejich disjunkce). Je pravdivá, pokud alespoň jeden prvek je pravdivý. Prázdná klauzule □ je vždy nepravdivá — neobsahuje žádný pravdivý prvek. Příklad klauzule <math>\{p, \neg q, r\}</math> dříve značeno <math>(p \vee \neg q \vee r)</math>.
  * **formule** je (ne nutně konečná) množina klauzulí (chápána jako jejich konjunkce, tedy KNF). Je pravdivá, je-li každý její prvek pravdivý. Prázdná formule ∅ je vždy pravdivá — neobsahuje žádný nepravdivý prvek. Příklad formule <math>\{\{ \neg q\},\{ \neg p, q\}\}</math> dříve značeno <math>\neg q \wedge ( \neg p \vee q)</math>.
  * **rezoluční pravidlo**: nechť <math>C_1 \ = \ \{p\} \ \sqcup \ C'_1, \ C_2 \ = \ \{ \neg p \} \ \sqcup \ C'_2</math> jsou klauzule, jejich rezolventou je <math>C \ = \ C'_1 \ \cup \ C'_2</math>. Rezoluční pravidlo zachovává splnitelnost, tj. libovolná valuace splňující C<sub>1</sub> a C<sub>2</sub> splňuje i C.
  * **rezoluční důkaz** klauzule C z formule S je konečná posloupnost klauzulí C<sub>1</sub>,C<sub>2</sub>,...,C<sub>n</sub>, kde C<sub>n</sub> = C a každé C<sub>i</sub> je buď prvkem S, nebo rezolventou klauzulí C<sub>j</sub>, C<sub>k</sub> pro j,k < i. Existuje-li tento důkaz, je C rezolučně dokazatelná z S (píšeme <math> S \ \vdash \ _R \ C</math>). Odvození □ z S je vyvrácením S.
[2]
</note>
Přehlednější reprezentací rezolučních důkazů jsou stromy. **Strom rezolučního důkazu** C z S je binární strom T s vlastnostmi:
  * kořenem T je C
  * listy T jsou prvky S
  * libovolný vnitřní uzel C<sub>i</sub> s bezprostředními následníky C<sub>j</sub>, C<sub>k</sub> je rezolventou C<sub>j</sub>, C<sub>k</sub>.

Příklad: strom důkazu <math>C \ = \ \{\neg q\}\ z\ S\ =\ \{\{p,r\},\{\neg q,\neg r\},\{\neg p\}\}</math>
{{:home:inf:ap4_rezoluce_pr.jpg|}}

<note tip>Obecné schéma důkazu, formule A je log. důsledkem množiny formulí T:
  - vytvoříme konjunkci T' všech prvků z T,
  - formuli T' ∧ ¬A převedeme do KNF a
  - ukážeme KNF(T' ∧ ¬A) <math>\vdash \ _R </math> □.
</note>
**Výhody pro strojové zpracování**:
  * systematické hledání důkazu
  * práce s jednoduchou datovou strukturou
  * jediné odvozovací pravidlo

**Problém**: Strategie generování rezolvent — prohledávaný prostor může být příliš veliký. Omezení prohledávaného prostoru (**zjemnění rezoluce**):
  * ukončením prohledávání neperspektivních cest
  * určením pořadí při procházení alternativních cest
Doposud [2].

**Lineární rezoluce** –- jde o posloupnost dvojic <math><C_{0}, B_{0}></math>, ... ,  <math><C_{n}, B_{n}></math> takovou, že <math>C = C_{n+1}</math>  a 
  - <math>C_{0}</math> a všechny <math>B_{i}</math> jsou z S anebo nějaké <math>C_{j}</math>, kde <math>j<i</math>
  - každé <math>C_{i+1}</math>, <math>i \leq n</math> je rezolventou <math>C_{i}</math> a <math>B_{i}</math> (vstupní klauzule S, boční <math>B_{i}</math> a střední <math>C_{i}</math>)
  * je korektní a úplná

**Lineární vstupní rezoluce** (LI) množiny <math>S=P \cup \{ G\}</math> je lineární vyvrácení S, které začíná klauzulí G, a bočními klauzulemi jsou jen klauzule z P. 
  *je úplná jen pro Hornovy klauzule((klauzule s nejvýše jedním pozitivním literálem))

**LD rezoluce** –- už máme uspořádané klauzule a při rezoluci vkládáme dovnitř. LD rezoluční vyvrácení <math>P \cup \{ G\}</math> je postupnost <math><G_{0}, C_{0}></math>, ... , <math><G_{n}, C_{n}></math> uspořádaných klauzulí taková, že <math>G_{0}=G, G_{n+1}=</math>□, <math>C_{i} \in T</math> a každé <math>G_{i}</math>,  <math>1\leq i\leq n</math> je rezolventou uspořádaných klauzulí <math>G_{i-1}</math> a <math>C_{i-1}</math> 

[4]

===== Předměty =====

[[https://is.muni.cz/auth/predmety/predmet.pl?id=427608;|IB101]] Úvod do logiky a logického programování

===== Použitá literatura =====
[1] Štěpán, Jan, //Klasická logika//. Olomouc, Univerzita Palackého v Olomouci 2001.
[2] Popelínský, L., Mráková, E., //Úvod do logiky a logického programování//, slídy, červen 2008, dostupné na: http://www.fi.muni.cz/~popel/lectures/bak_logika/
[3] Raclavský, J., //Výroková logika//, červen 2008, dostupne na http://www.phil.muni.cz/fil/logika/vl.php
[4] Vypracování otázek Elena Halická - [[http://www.fi.muni.cz/~xhalic1/statnice/vypracovaneIM.doc]]

===== Kam dál? =====
[[http://kti.mff.cuni.cz/downloads/Pl_ps.zip|Volně stažitelné skripta z předmětu Výroková a predikátová logika na MFF UK od Petra Štěpánka]]

===== Vypracuje =====
Erik Zitterbart, ICQ: 172319825. eriksson (zavinac) mail.muni.cz
Z mé strany 99%. Rád dopracuji případné komentáře a opravy. Vypracování je poněkud delší.

Otázku si přečetl pan doc. RNDr. Lubomír Popelínský a rámcově prošel. Jeho podněty pro doplnění textu, opravy nesrovnalostí a odstranění matoucích či k otázce se nevztahujících textů byly do otázky zaneseny. Tato kontrola je jen **rámcová**, stále se může stát, že v otázce zůstala zapomenutá chybka či nesrovnalost, vyučující za toto nenese odpovědnost, berte tuto rámcovou kontrolu jako formu pomoci od vyučujících pro studenty.
~~DISCUSSION~~