Úvod a dokazovanie vo formálnom systéme.

Ciele

Oboznámiť sa s obsahom, priebehom a hodnotením cvičení.
Získať učebné materiály k predmetu.
Použiť Boolovu algebru a formálne systémy na dôkaz viet vo výrokovej logike.

Úvod

Predmet Formálne špecifikácie systémov je zameraný najmä na špecifikačné jazyky Petriho siete a B-Metóda a s nimi spojené analytické, vývojové a verifikačné prostriedky.

Postup

Cvičenia z predmetu sú rozdelené na 3 celky:
1. Dôkaz vo formálnej logike.
2. Petriho siete: reprezentácia, výpočet, výpočet invariantov, analýza dosiahnuteľnosti, typy Petriho sietí.
3. Verifikovaný vývoj softvéru: jazyk Guarded Commands a B-Metóda
Hodnotenie za semester pozostáva z
- Hodnotenia aktivity na cvičeniach (5b).
- Hodnotenia zadania (15b).
Zadanie bude z B-Metódy a bude zamerané na tvorbu riadiaceho modulu pre železničnú trať.
Stiahnite si doplnkové učebné texty k predmetu z http://hornad.fei.tuke.sk/~korecko/fss/SK_FSpodklady.pdf.
Oboznámte sa s obsahom dokumentu s teóriou k formálnej logike.
Určte povahu formúl (tzn. či formula je (ne)splniteľná alebo tautológia).
1. \(\neg P \vee Q\)
2. \((\neg P \vee Q) \wedge (R\rightarrow(P\leftrightarrow Q))\)
3. \((Q\rightarrow(P\vee Q))\)
4. \((R\rightarrow(P\vee R))\rightarrow (P \wedge \neg Q)\)
5. \((P\wedge(P \rightarrow R))\rightarrow R\)
Poznámka: Na riešenie použite pravdivostné tabuľky, definíciu funkcie pravdivostného ohodnotenia alebo prevod do Boolovej algebry. Aby ste sa zbavili implikácie a ekvivalencie, preveďte ich na ostatné propozicionálne spojky pomcou Def.2.2 z dokumentu s teóriou k formálnej logike.
Dokážte, že nasledujúce formuly sú teorémy výrokovej logiky.
1. Ak platí \(A \vee B\) potom platí aj \(B \vee A\)
2. Ak platí \(A\) a platí \(A \rightarrow B\), potom platí aj \(B\)
Poznámka: Na riešenie použite formálny systém z dokumentu teóriou k formálnej logike. V druhej teoréme \(A \rightarrow B\) zapíšte ako \((\neg A) \vee B\).

Zdroje