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
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