Matematická logika

Na těchto strankách budu vyvěšovat pdf soubory s tím, co bude promítáno na přednášce a další informace k předmětu Y01MLO.

Přednášky:

• 1. přednáška - Relace
• 2. přednáška - Mohutnost množin
• 3. přednáška - Výroková logika
• 4. přednáška - Tautologická ekvivalence, normalní formy
• 5. přednáška - Rezoluce ve výrokové logice
• 6. přednáška - Predikátová logika, ucelený text
• 7. přednáška - Prenexní normalní tvar formule
• 8. přednáška - Skolemova normalní forma
• 9. přednáška - Herbrandova věta
• 10. přednáška - Rezoluce v predikátové logice
• 11-12. přednáška - Příklady na rezoluci v predikátové logice

Cvičení:

• Příklady 1 - pár řešených příkladů na procvičování.
• Příklady 2 - pár řešených příkladů na procvičování.

Zkoušky:

• Informace o zkouškách

Užitečné odkazy:

• Y01MLO - oficiální osnova předmětu.
• Další informace - informace o předmětu z minulých let, obsahuje také nějaké studijní materiály.

  Další zajímavé odkazy:

• Prover9 a Mace4 - www stránky automatických dokazovačů, které jsem ukazoval na přednášce. Dokazovač Prover9 používá resoluční metodu. Volně ke stažení.
• Příklady souborů pro Prover9 a Mace4, které jsem ukazoval na přednášce: Lháři a Obarvování grafů.

Literatura:

• M. Demlová, B. Pondělíček: Matematická logika. ČVUT Praha, 1997.
• Velmi jemný úvod do matematické logiky - elektronické skripta od J.Velebila.

  Další zajímavá literatura:

• V. Švejdar: Logika: neúplnost, složitost a nutnost. Academia Praha, 2002. (ke stažení zde)
• A. Sochor: Klasická matematická logika. Karolinum, 2001.
• J. Gallier: Logic for Computer Science: Foundations of Automatic Theorem Proving, Wiley, 1986. (ke stažení zde)
• L. van den Dries: Logic notes. (dvi soubor)
• L. Bachmair, H. Ganzinger: A Theory of Resolution. Research Report MPI-I-97-2-005, Max-Planck-Institut für Informatik, 1997. (ps soubor)