CourseWare Wiki
Search
Log In
old
courses
a4m33au
priprava_na_zkousku
Warning
This page is located in archive.
Differences
This shows you the differences between two versions of the page.
View differences:
Side by Side
Inline
Go
Link to this comparison view
Both sides previous revision
Previous revision
2012/02/26 13:11 pudlapet
2011/08/20 19:38 pudlapet
2011/08/20 19:37 pudlapet priklady z minulych pisemek
2011/06/24 20:10 pudlapet
2011/06/24 19:05 pudlapet
2011/06/24 19:02 pudlapet created
Go
Next revision
Previous revision
2012/02/26 13:11 pudlapet
2011/08/20 19:38 pudlapet
2011/08/20 19:37 pudlapet priklady z minulych pisemek
2011/06/24 20:10 pudlapet
2011/06/24 19:05 pudlapet
2011/06/24 19:02 pudlapet created
Go
Next revision
Both sides next revision
courses:a4m33au:priprava_na_zkousku [2011/06/24 19:05]
pudlapet
courses:a4m33au:priprava_na_zkousku [2011/08/20 19:37]
pudlapet
priklady z minulych pisemek
Line 7:
Line 7:
- Jedná-li se o otevřenou úlohu (např. logické hádanky - kdo je poctivec apod.), formulujte hypotézu jako formuli.
- Jedná-li se o otevřenou úlohu (např. logické hádanky - kdo je poctivec apod.), formulujte hypotézu jako formuli.
- Snažíte-li se dokázat splnitelnost formulí (neplatnost domněnky), hledejte model.
- Snažíte-li se dokázat splnitelnost formulí (neplatnost domněnky), hledejte model.
-
- Snažíte-li se dokázat nesplnitelnost formulí (platnost domněnky)
,
převeďte formule a znegovanou hypotézu na klauzule
a
pomocí rezolučního kalkulu hledejte spor.
+
- Snažíte-li se dokázat nesplnitelnost formulí (platnost domněnky)
:
+
-
převeďte formule a znegovanou hypotézu na klauzule
,
+
-
pomocí rezolučního kalkulu hledejte spor
;
+
- při provádění důkazu používejte zpětnou a dopřednou subsumpci - jednak procvičíte pojem subsumpce a jednak tím velmi často zjednodušíte důkaz
.
- Jedná-li se o úlohu s hypotézou, v rámci procvičení hypotézu odstraňte a ponechte pouze axiomy; tato množina formulí bude splnitelná; najděte její model.
- Jedná-li se o úlohu s hypotézou, v rámci procvičení hypotézu odstraňte a ponechte pouze axiomy; tato množina formulí bude splnitelná; najděte její model.
-
V případě
,
že
máte problémy
:
+
====
V případě
problémů ====
-
*
s klauzifikací
: zapi
šte formule v TPTP a spusťte na soubor <code sh>eprover --cnf soubor</code> který provede klauzifikaci.
+
Mů
že
pomoci využít pro problematickou část úlohy odpovídající nástroj (viz. níže). Jeho výstup pak porovnat s vlastními pokusy a s teorií. Zkusit pak znovu danou část úlohy provést samostatně.
-
*
s dokazováním rezolučním kalkulem
: následující
shell skript převede formule z TPTP na standardním vstupu do jazyka knihovny LADR, nastaví parametry tak, aby dokazovač prováděl neoptimalizovanou binární rezoluci (takže jsou vidět jednotlivé kroky) a spustí Prover9:
+
+
Při problémech
:
+
===
s klauzifikací
===
+
Zapi
šte formule v TPTP a spusťte na soubor <code sh>eprover --cnf soubor</code> který provede klauzifikaci.
+
===
s dokazováním rezolučním kalkulem
===
+
Následující
shell skript převede formule z TPTP na standardním vstupu do jazyka knihovny LADR, nastaví parametry tak, aby dokazovač prováděl neoptimalizovanou binární rezoluci (takže jsou vidět jednotlivé kroky) a spustí Prover9:
<code sh>
<code sh>
#!/bin/bash
#!/bin/bash
Line 25:
Line 33:
) | prover9
) | prover9
</code>
</code>
-
*
s hledáním modelů
: najd
ěte model pomocí hledače modelů Paradox nebo Mace4, a poté ručně ověřte, že se skutečně jedná o model, tedy že všechny formule jsou ve výsledné interpretaci splněny.
+
-
Výstup
z
nástroje porovnejte se svými pokusy a srovnejte s teorií. Zkuste znovu danou část provést sami,
př
ípadně zvolte jednodu
š
ší úlohu
.
+
===
s hledáním modelů
===
+
Najd
ěte model pomocí hledače modelů Paradox nebo Mace4, a poté ručně ověřte, že se skutečně jedná o model, tedy že všechny formule jsou ve výsledné interpretaci splněny.
+
+
===== Příklady
z př
ede
š
lých písemek =====
+
Jako bonus příklady z minulých písemek:
+
- {{:courses:a4m33au:pisemka_1.pdf|}}
+
- {{:courses:a4m33au:pisemka_2
.
pdf|}}
courses/a4m33au/priprava_na_zkousku.txt
· Last modified: 2013/10/04 13:02 (external edit)