Differences

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

--- courses:a4m33au:priprava_na_zkousku [2011/08/20 19:38]
pudlapet
+++ courses:a4m33au:priprava_na_zkousku [2013/10/04 13:02]
@@ Line 1: / Line 1: @@
-====== Příprava na zkoušku ======
-Náměty na cvičení, která vám pomohou připravit se ke zkoušce.
-===== Úlohy z přednášky a cvičení =====
-Projděte si úlohy z výrokové i predikátové logiky, které byly řešeny na cvičení nebo ukazovány na [[start#Materiály z přednášek|přednášce]], včetně těch nejjednodušších.
-  - Je-li úloha slovní, nejprve ji formalizujte v logice 1. řádu či ve výrokové logice.
-  - 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,
-    - 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ě problémů ====
-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ě.
-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
-(
-    cat <<EOF
-set(raw).
-set(binary_resolution).
-set(print_kept).
-set(print_gen).
-EOF
-    tptp_to_ladr
-) | 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.
-===== 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|}}