Cvičení - Výpočtová logika (IA008)

Ukončení

Cvičení není ukončeno udělením zápočtu, nicméně účast na něm je povinná pro udělení povolení absolvovat závěrečnou zkoušku z předmětu. Jsou povoleny dvě neomluvené neúčasti.

Obsah cvičení

• Příklady do cvičení (english version). Tyto příklady si prosím vytiskněte a noste do cvičení. Postupně (po procvičení určitých větších celků) se na této stránce objeví i řešená verze této sbírky příkladů.
• 1. cvičení (25. 2. 2009): Převod formulí výrokové logiky do disjunktivní normální formy (DNF) a konjunktivní normální formy (CNF), rezoluce ve výrokovém počtu a převod formulí predikátové logiky do prenexní normální formy (PNF).
• 2. cvičení (4. 3. 2009): Skolemizace. Transformace úkolu Dokažte, že daná formule je logickým důsledkem dané množiny sentencí do klauzulární formy. Unifikace, rezoluce v predikátové logice.
• 3. cvičení (11. 3. 2009): Zjemnění rezoluce (lineární rezoluce, lineární vstupní rezoluce, LD-rezoluce, SLD-rezoluce), Hornovy klauzule.
• 4. cvičení (18. 3. 2009): SLD-stromy, vztah jazyka Prolog k rezolučním důkazům, syntax jazyka Prolog. Programování v jazyce Prolog a práce se seznamy.
• 5. cvičení (25. 3. 2009): Blokový model (box model), trasování, řez. Zajímavé aplikace v prologu: eliza.pl, marvin, quarto, sudoku.pl (řeší toto zadání).
• 1. 4. 2009 cvičení nejsou (týká se skupin IA008/01 a IA008/02).
• 6. cvičení (8. 4. 2009): Gramatiky definitních klauzulí. Materiály ke stažení (link do ISu).
  Gramatiky prezentované na cvičení:

  grammar_eng.pl	anglické věty
  grammar.pl	chybná a dvě opravené gramatiky pro vyhodnocování jednoduchých aritmetických výrazů
  aba.pl	gramatika pro jazyk {anbnan | n≥0}

• 7. cvičení (15. 4. 2009): Atomická tabla, systematická tabla a tablové důkazy ve výrokové logice.
• 8. cvičení (22. 4. 2009): Tabla pro predikátovou logiku.
• 9. cvičení (29. 4. 2009): Tabla pro modální logiku.
• 10. cvičení (6. 5. 2009): Induktivní logické programování.
• Řešení příkladů ze všech cvičení (PDF)
• 11. cvičení (13. 5. 2009): Prezentace důkazových systémů leanTaP a ACL2.
• 20. 5. 2009 jsou konzultace (účast není povinná).

Poznámka: Naleznete-li v materiálech chyby, nahlaste je prosím cvičícímu.

Prolog

Na FI MUNI je k dispozici implementace programovacího jazyka Prolog zvaná SICStus Prolog (najdete ji v modulu sicstus). K  dalším rozšířeným distribucím patří např. SWI Prolog a Yap Prolog.

Při spuštění systémů SICStus a Yap můžeme k načtení předložit soubor s programem:

      sicstus -l zdroj[.pl]
      yap -l zdroj[.pl]

Po spuštění inerpreteru pak lze načíst program zadáním nějakého z dotazů:

      ?- [zdroj1,'zdroj2.pl'].
      ?- consult([zdroj1,'zdroj2.pl']).
      ?- reconsult([zdroj1,'zdroj2.pl']).
      ?- compile([zdroj1,'zdroj2.pl']).
      ?- recompile([zdroj1,'zdroj2.pl']).

Řada predikátů je dostupná přímo v distribucích jazyka. Je však nutné je načíst. V případě SICStus a Yap to provedeme příkazem use_module/1. Např. use_module(library(list)). načte predikáty pro práci se seznamy.

Dotazy interpretru zadáváme v podobě atomických formulí oddělených čárkou a s tečkou na konci.

      ?- use_module(library(list)).
         [ reconsulting /packages/local/Yap-4.4.4/share/Yap/lists.yap... ]
         [ reconsulted /packages/local/Yap-4.4.4/share/Yap/lists.yap in module lists, 10 msec 18024 bytes ]
         yes
        
      ?- reverse([a,b,c],X).
         X = [c,b,a] ? 
         yes

      ?- sort([2,5,1,3,9,0],X),reverse(X,Y),length(Y,L).
         L = 6,
         X = [0,1,2,3,5,9],
         Y = [9,5,3,2,1,0] ? ;
         no

Interpreter se ukončí stiskem kláves <Ctrl> + d.

Literatura

• Fitting, Melvin. First order logic and automated theorem proving [1996]. 2^nd ed. New York: Springer, 1996. xvi, 326 pages. Graduate texts in computer science. ISBN 0-387-94593-8.
• Jirků, Petr a Vejnarová, Jiřina: Logika (Neformální výklad základů formální logiky). Skriptum VŠE Praha, 2000. 161 stran. ISBN 80-245-0054-X http://www.cuni.cz/~jirkup/logika/logika2.ps
• Nerode, Anil and Shore, Richard A. Logic for applications. New York: Springer-Verlag, 3. xvii, 365. Texts and Monographs in Computer Science. ISBN 0-387-94129-0.
• Šerák, Jan. Logika: zápisy z přednášky Jiřího Zlatušky.
• Štěpán, Jan. Klasická logika. VUP Olomouc, 2001 198 stran. ISBN 80-244-0254-8.
• Zlatuška, J. Logika, logické programování a paralelismus. (Logic, logic programming and paralelism, in Czech), UVT MU, 1991, 50 pp.