Differences

This shows you the differences between two versions of the page.

--- courses:a4m33au:priprava_na_zkousku [2011/06/24 19:05]
pudlapet
+++ courses:a4m33au:priprava_na_zkousku [2011/08/20 19:38]
pudlapet
@@ Line 7: / Line 7: @@
   - 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 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.
-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>
 #!/bin/bash
@@ Line 25: / Line 33: @@
 ) | prover9
 </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|}}