456-0535/01 – Úvod do logiky (UDL)
| Garantující katedra | Katedra informatiky | Kredity | 6 |
| Garant předmětu | prof. RNDr. Marie Duží, CSc. | Garant verze předmětu | prof. RNDr. Marie Duží, CSc. |
| Úroveň studia | pregraduální nebo graduální | Povinnost | povinný |
| Ročník | 1 | Semestr | letní |
| | Jazyk výuky | čeština |
| Rok zavedení | 1999/2000 | Rok zrušení | 2009/2010 |
| Určeno pro fakulty | FEI | Určeno pro typy studia | bakalářské |
Cíle předmětu vyjádřené dosaženými dovednostmi a kompetencemi
Cilem predmetu je seznamit studenty s pojmovym aparatem a metodami vyrokove logiky a predikatove logiky 1. radu.
Vyučovací metody
Anotace
Predmet pokryva zakladni pojmovy aparat a metody vyrokove logiky a predikatove logiky 1. radu. Student bude rovnez seznamen s metodami automatickeho dokazovani a odvozovani. Tento aparat a metody jsou bezne pouzivany v ruznych oblastech informatiky (precizace a formalizace intuitivnich poznatku a teorii, jazyky logickeho programovani, umela inteligence ...) a v mnoha jinych exaktnich disciplinach.
Povinná literatura:
Stepan, J.: Logika a logicke systemy. Votobia Olomouc, 1992.
Manna, Z.: Matematicka teorie programu;. SNTL Praha, 1981.
Gaher, F.: Logika pre kazdeho. IRIS Bratislava, 1998.
Gaher, F.: Logicke hadanky a paradoxy. IRIS Bratislava, 1997.
Smullyan, R.M.: Jak se jmenuje tahle knížka? Mladá Fronta, Praha 1986.
Lukasova, A.: Logicke zaklady umele inteligence. Skripta Ostravska universita, 1997.
Metakides, G. - Nerode, A.: Principles of Logic and Logic Programming. North-Holland, 1996.
http://www.cs.vsb.cz/duzi/ Courses
Doporučená literatura:
http://www.phil.muni.cz/fil/logika/
Další studijní materiály
Forma způsobu ověření studijních výsledků a další požadavky na studenta
Průběžná kontrola studia:
Pisemna proverka ze semantickych metod VL - max. 15 bodu, minimalne 5 bodu.
Pisemna proverka ze semantickych metod PL - max. 15 bodu, minimalne 5 bodu.
Podmínky udělení zápočtu:
Ziskani alespon 15 bodu.
E-learning
Další požadavky na studenta
Prerekvizity
Předmět nemá žádné prerekvizity.
Korekvizity
Předmět nemá žádné korekvizity.
Osnova předmětu
Přednášky:
Uvod do logiky. O cem je logika? Kde vsude nam muze logika pomoci. Logika jako veda o spravne argumentaci: logicke vyplyvani, usudky.
Jazyk vyrokove logiky (abeceda a gramatika). Definice spojek vyrokove logiky.
Prevod z prirozeneho jazyka do symbolickeho jazyka vyrokove logiky. Semantika vyrokove logiky: pravdivostni ohodnoceni, tautologie, kontradikce, splnitelnost.
Vyrokove logicke vyplyvani. Semanticke metody overovani spravnosti usudku ve vyrokove logice.
Uplny system spojek vyrokove logiky, veta o reprezentaci, normalni formy formuli vyrokove logiky, vety o funkcni uplnosti, logicke dusledky mnoziny formuli.
Rezolucni odvozovani ve vyrokove logice a jeho vyuziti.
Spravne usudky, ktere nelze analyzovat na zaklade vyrokove logiky. Jazyk predikatove logiky prvniho radu. Volne a vazane promenne, substituovatelnost termu za promenne.
Semantika predikatove logiky prvniho radu, pojem interpretace a modelu. Prevod z prirozeneho jazyka do symbolickeho jazyka predikatove logiky prvniho radu.
Splnitelnost formuli, (logicka) pravdivost, nesplnitelnost, logicke vyplyvani. Tautologie predikatove logiky prvniho radu.
Semanticke metody overovani spravnosti usudku. Tradicni Aristotelova logika.
Dedukce v predikatove logice prvniho radu. Modely a logicke dusledky. Splnovani a pravdivost v predikatove logice, metody semanticke analyzy, semanticka tabla. Nerozhodnutelnost problemu logicke pravdivosti v predikatove logice.
Formalni systemy. Uvod - charakteristika a vlastnosti formalnich systemu. Mnozina axiomu a teoremu. Pojem dukazu ve formalnim systemu. Uplnost predikatove logiky 1. radu.
Teoreticke zaklady logickeho programovani. Prenexni normalni formy formuli, Skolemova klauzularni forma, Herbrandova procedura - zakladni rezolucni metoda.
Obecna rezolucni metoda a unifikacni algoritmus.
Cvičení:
Priklady usudku formulovanych v prirozenem jazyce
Prevod vet z prirozeneho jazyka do jazyka vyrokove logiky
Negace vet ve vyrokove logice
Semanticke metody overovani spravnosti usudku VL (tabulkou, sporem, Quinova metoda)
Prevod formuli VL do normalnich forem
Hledani logickych dusledku mnoziny formuli VL
Rezolucni odvozovani ve vyrokove logice a jeho vyuziti.
Prevod z prirozeneho jazyka do jazyka PL 1. radu
Negace tvrzeni, ekvivalentni transformace
Semanticke metody overovani spravnosti usudku
Pojem interpretace a modelu
Prevod formuli do Skolemovy normalni formy
Rezolucni metoda v PL 1. radu
Dukazy v Gentzenove systemu, prirozena dedukce
Podmínky absolvování předmětu
Výskyt ve studijních plánech
Výskyt ve speciálních blocích
Hodnocení Výuky
Předmět neobsahuje žádné hodnocení.