To jest stara wersja strony!

ψ

# Kurs z Logiki

## Logic for Computer Science: 2020

1. Introduction to the Course. Goals and principles. Introduction to Logic. Basics of Propositional Calculus. Example syntax and a note on interpretation/semantics. Example inference rules. Elements of Big Picture. Examples of problems and their solutions. [26.02.2020; ALi]
2. Propositional Calculus. Syntax and Sematics. Logical consequence and logical equivalence. Truth tables and their analysis. Selected Boolean Functions. Functional Completeness. Properties of logical formulas. [4.03.2020; ALi]
Uwaga: Zajęcia odwołane 11.03.2020 godz. 10:00 do 24/25(?).03.2020! Attention: Lectures/classes cancelled until March 24/25-th(?), 2020! See: AGH - Decision/Decycja We switch to asynchronous, on-line course. Topics, dates, and selection of material are presented in steel-blue.
3. Logical equivalence. Transformations of formulas: equivalent transformation rules. Minterms and maxterms. Normal forms: CNF, DNF, NNF. Implicants and implicents. Minimal representation. [11.03.2020 (online course; lecture 2 below)]
4. Automated Inference and Theorem proving. Logical inference methods. Derivation and proof. Rules of inference. Formal proofs. The Fitch System. Semantic Tableau. Resolution in Propositional Calculus. Dual Resolution. [18.03.2020 (online course; lecture 3 below)]
5. The role of CNF. The SAT problem. Approaches to solving the SAT problem. Decision trees. OBDD diagrams. SAT solvers. [25.03.2020; lecture 4 below]
6. Boolean Algebra. Function syntehsis. The CNF and DNF again: the Pi and Sigma notations. Finding minimal representations. Logical circuits systnthesis. Karnaugh Tables. The Quine-McCluskey algorithm.
7. First -Order Logic. Syntax and Semantix. Logical transformation Rules. Logical inference rules. The Fitch system for FOPC.
8. CNF and DNF in FOPC. Transformations to S-form. Herbrand Base. Substituion and unification. Resolution in FOPC.
9. Introduction to logic programming. Prolog. Constraint Programming. Multi-valued logics. Fuzzy logic. Temporal and modal logics. Description logics.

Yet another chance:

Rough lecture notes in .pdf (for cautious, personal use only):

## Plan wykładu z logiki: 2018

2. Unicorn - rozwiązanie. Wprowadzenie do rachunku zdań (Propositional Calculus). Składnia, semantyka. Pojęcie interpretacji i logicznej konsekwencji. Równoważność logiczna formuł. [9.03.2018: ALi]
3. Rachunek zdań: składnia, semantyka. Pojęcie interpretacji i logicznej konsekwencji. Funkcje logiczne. Systemy logiczne funkcjonalnie pełne. Transformacje zachowujące równoważność. Analiza formuł metodą zero-jedynkową. Zastosowanie transformacji równoważnościowych - przykład. [16.03.2018: ALi]
4. Mintermy i makstermy. Postacie CNF, DNF, NNF. Implikanty i implicenty. Interpretacja postaci CNF i DNF. Zastosowania. Przykład wyznaczania i redukcji implikantów i implicentów. [23.03.2018;ALi]
5. [30.03.2018 - wolne na Święta: Wielkanoc!]
6. E-learning: wyznaczyć implikanty i implcenty dla modelu Unicorn. [6.04.2018; ALi]
7. Reguły wnioskowania. Metody dowodzenia w rachunku zdań. Metoda rezolucji i jej zastosowania. Metoda rezolucji dualnej. Semantic Tableau. System Fitcha. Badanie spełnialności - drzewa decyzyjne i ich redukcja. Diagramy OBDD. Problem SAT i SAT-Solvery [13.04.2018; ALi]
8. Metoda Semantic Tableau. System Fitcha. Badanie spełnialności - drzewa decyzyjne i ich redukcja. Diagramy OBDD. Problem SAT i SAT-Solvery: Unicorn revisited. [20.04.2018; ALi]
9. Synteza układów logicznych.Implikanty i implicenty: minimalizacja funkcji. Tabele Karnaugha. Metoda Quine'a-McCluskey. Układy statyczne i dynamiczne. [27.04.2018]
10. Rachunek predykatów pierwszego rzędu. Składnia i semantyka. Zmienne i termy; kwantyfikatory. Interpretacja i wartościowanie. Interpretacja Herbranda. Twierdzenie Herbranda. Pełność krp z ideą dowodu. Twierdzenia Skolema-Lowenheima. Nierozstrzygalność. Przykłady. [11.05.2018; ALi]
11. Juwenalia - godziny rektorskie [18.05.2018]
12. Dowodzenie w rachunku predykatów. System Fitcha. Metoda rezolucji w rachunku predykatów. Wstęp do programowania logicznego. Język Prolog. Logiki atrybutowe i opisowe. Programowanie z ograniczeniami. [25.05.2018]
13. Aktualne kierunki rozwoju. Logiki temporalne i rozmyte. Logiki atrybutowe i opisowe. Zastosowania. Big Picture. [???]

—- Egzaminy 2018:

• Terminy egzaminów - logika I rok: sala H-24/B-1.
• 28.06 (czwartek) 15:00-19:00 (2 grupy po 2h),
• 03.07 (wtorek) 11:00-15:00 (1 lub 2 grupy po 2 h).

## Plan wykładu z logiki: 2017

2. Wprowadzenie do rachunku zdań (Propositional Calculus). Składnia, semantyka. Pojęcie interpretacji i logicznej konsekwencji. Równoważność logiczna formuł. [10.03.2017: ALi]
3. Funkcje logiczne. Systemy logiczne funkcjonalnie pełne. Transformacje zachowujące równoważność. Analiza formuł metodą zero-jedynkową. Mintermy i makstermy. Postacie CNF i DNF. [17.03.2017: ALi]
4. Postacie CNF, DNF, NNF. Interpretacja postaci CNF i DNF. Zastosowania. Reguły wnioskowania. Metody dowodzenia w rachunku zdań. [24.03.2017;ALi]
5. Metoda rezolucji i jej zastosowania. Metoda rezolucji dualnej. Semantic Tableau. System Fitcha. Badanie spełnialności - drzewa decyzyjne i ich redukcja. Diagramy OBDD. Problem SAT i SAT-Solvery [31.03.2017; ALi]
6. Wybrane zaawansowane zagadnienia KRZ. Systemy Hilberta. [7.04.2017] [KJo]
7. [21.04.2017] E-Learning.
9. Rachunek predykatów pierwszego rzędu. Składnia i semantyka. Zmienne i termy; kwantyfikatory. Interpretacja i wartościowanie. Interpretacja Herbranda. Twierdzenie Herbranda. Pełności krp z ideą dowodu. Twierdzenia Skolema-Lowenheima. Nierozstrzygalność. Przykłady. [5.05.2017;KJo]
10. Logika Juwenaliów [12.05.2017: godziny rektorskie].
11. Dowodzenie w rachunku predykatów. System Fitcha. Metoda rezolucji w rachunku predykatów. Wstęp do programowania logicznego. Język Prolog. Logiki atrybutowe i opisowe. Programowanie z ograniczeniami.
12. Aktualne kierunki rozwoju. Logiki temporalne i rozmyte. Logiki atrybutowe i opisowe. Zastosowania. Big Picture.

—- Egzaminy 2017:

• Terminy egzaminów - logika I rok: 23.06 i 30.06 + 8.09 2 x 2 h s. H-24

### Plan wykładu z logiki: 2016

2. Rachunek zdań. Składnia, semantyka. Pojęcie interpretacji i logicznej konsekwencji. Funkcje logiczne. Systemy logiczne funkcjonalnie pełne. Transformacje zachowujące równoważność. Analiza formuł metodą zero-jedynkową. [4.03.2016: ALi]
3. Wstęp do aksjomatycznego ujęcia KRZ i dowodów metodą aksjomatyczną; twierdzenie o dedukcji. [11.03.2016; KJo]
4. Aksjomatyczne ujęcie KRZ-kontynuacja; KRZ w ujęciu metalogicznym (twierdzenie o pełności, zwartości, niesprzeczności). [18.03.2016; KJo]
5. Postacie CNF, DNF, NNF. Reguły wnioskowania. Metody dowodzenia w rachunku zdań. [1.04.2016; ALi]
6. Metoda rezolucji i jej zastosowania. Metoda rezolucji dualnej. Semantic Tableau. System Fitcha. [8.04.2016: ALi]
7. Badanie spełnialności - drzewa decyzyjne i ich redukcja. Diagramy OBDD. Problem SAT i SAT-Solvery. Programowanie z ograniczeniami. Synteza układów logicznych. Tabele Karnaugha. [15.04.2016: ALi]
8. Rachunek predykatów pierwszego rzędu. Składnia i semantyka. Zmienne i termy; kwantyfikatory. Interpretacja i wartościowanie. Interpretacja Herbranda. Przykłady. [22.04.2016; ALi]
9. Dowodzenie w rachunku predykatów. System Fitcha. Metoda rezolucji w rachunku predykatów. Wstęp do programowania logicznego. Język Prolog. Logiki atrybutowe i opisowe. [6.05.2016; ALi]
10. Ważne wyniki logiki (Tw. Gödla). Big Picture. Logiki modalne i temporalne. Logiki wielowartościowe. Wielcy Polscy Logicy [20.05.2016; KJo]

Egzaminy 2016:

• Termin I: 27.06.2016, 13:00-17:00 sala H-24 [egzamin pisemny; 2 grupy]
• Termin II: 30.06.2016, 9:00-13:00 sala 224 C-2 [egzamin pisemny; 1 lub 2 grupy]

3. Elementy podejścia systemowego: model, wejścia, wyjścia, cel. Zastosowania logiki. [18.03.2015]
5. Składnia i semantyka rachunku zdań. Interpretacje i modele. Równoważność. Przykłady modeli logicznych. [1.04.2015]
6. Interpretacja formuł rachunku zdań. Tabele prawdy. Równoważność i wynikanie. Definicje spójników. Systemy funkcjonalnie pełne. [8.04.2015]
7. Weryfikacja tautologii i konsekwencji logicznej w oparciu o tabele prawdy. Mintermy i makstermy. Klauzule Horna. [15.04.2015]
8. Postacie CNF, DNF i NNF i ich znaczenie. Sprowadzanie formuły do CNF, DNF i NNF. Implikanty i implicenty. [22.04.2015]
9. Reguły wnioskowania. Metody dowodzenia twierdzeń. Twierdzenia o dedukcji. Przykłady. [29.04.2015]
10. Rezolucja i rezolucja dualna. Zbiór logicznych konsekwencji. Metoda tablic semantycznych. Systemy Gentzenowskie. Drzewa decyzyjne. Diagramy OBDD.[6.05.2015]
11. Rachunek predykatów I rzędu.Składnia i semantyka [13.05.2015]
12. Rachunek predykatów I rzędu. Postacie CNF, DNF, NNF. Reguły przekształceń formuł z kwantyfikatorami. [27.05.2015]
13. Rachunek predykatów I rzędu. Podstawienia, unifikacja i rezolucja. [3.06.2015]
14. Zastosowania logiki. Język Prolog. Przykłady programów logicznych. Logiki nieklasyczne. [10.06.2015]

2. Elementy podejścia systemowego: model, wejścia, wyjścia, cel. Zastosowania logiki. [12.03.2014]
4. Składnia i semantyka rachunku zdań. Równoważność logiczna a logiczna konsekwencja. Przykłady modeli logicznych. [26.03.2014]
5. Interpretacja formuł rachunku zdań. Tabele prawdy. Równoważność i wynikanie. Definicje spójników. Systemy funkcjonalnie pełne. [2.04.2014]
6. Weryfikacja tautologii i konsekwencji logicznej w oparciu o tabele prawdy. Mintermy i makstermy. Klauzule Horna. [9.04.2014; K.G-D]
7. Postacie CNF, DNF i NNF i ich znaczenie. Sprowadzanie formuły do CNF, DNF i NNF. Implikanty i implicenty. [16.04.2014]
8. Algebra Boole'a. Funkcje Boolowskie. Synteza układów. Bramki logiczne. Tablice Karnaugha. [23.04.2014]
9. Reguły wnioskowania. Metody dowodzenia twierdzeń. Twierdzenia o dedukcji. Przykłady. [30.04.2014]
10. Rezolucja i rezolucja dualna. Zbiór logicznych konsekwencji. Tablice Karnaugha, sklejanie, minimalizacja. Metoda Quine-McCluskey'a. [7.05.2014]
11. Drzewa decyzyjne. Diagramy OBDD. Metoda tablic semantycznych. Dedukcja naturalna. [14.05.2014].
12. Rachunek predykatów I rzędu.Składnia i semantyka [21.05.2014]
13. Rachunek predykatów I rzędu. Postacie CNF, DNF, NNF. Reguły przekształceń formuł z kwantyfikatorami. [28.05.2014]
14. Rachunek predykatów I rzędu. Podstawienia, unifikacja i rezolucja. [4.06.2014]
15. Zastosowania logiki. Język Prolog. Przykłady programów logicznych. Logiki nieklasyczne. [11.06.2014]

Materiały do wykładów - wersja robocza (.pdf)

Polecane materiały - e-learning

2. Rachunek predykatów I rzędu i Metoda Rezolucji (Google Preview) KRR: Ronald Brachman book
3. Rachunek predykatów I rzędu i Metoda Rezolucji KRR - slides

1. Wprowadzenie do logiki. E-learning. [27.02.2013]
2. Elementy logiki w ujęciu systemowym. [6.03.2013]
3. Podstawowe koncepcje logiki. Składnia. Semantyka. Wnioskowania. [13.03.2013]
4. Rachunek zdań. Składnia. Semantyka. Logiczna konsekwencja. Równoważność. [20.03.2013]
5. Rachunek zdań. Funkcje logiczne. Systemy funkcjonalnie pełne. Transformacje zachowujące równoważność. [27.03.2013]
6. Logic Course at Stanford [3.04.2013 - e-learning]
7. Rachunek zdań. Postacie CNF, DNF, NNF. [10.04.2013]
8. Reguły wnioskowania. Wywód. Dowodzenie twierdzeń. Rezolucja. Rezolucja dualna. [17.04.2013]
9. Algebra Boole'a. Minimalizacja funkcji logicznych. Tablice Karnaugha. Algorytm Quine'a-McCluskeya. [24.04.2013].
10. E-learning: Rachunek zdań. Powtórzenie, usystematyzowanie i uzupełnienie wiadomości [8.05.2013]
11. Drzewa decyzyjne. Diagramy OBDD. Metoda tablic semantycznych. Dedukcja naturalna. [15.05.2013].
12. Rachunek predykatów I rzędu. [22.05.2013]
13. E-learning: Metoda rezolucji. [29.05.2013]
14. Metoda Rezolucji. Metoda rezolucji dualnej. Prolog i programowanie w logice. Ograniczenia logik klasycznych. Logiki nieklasyczne. [5.06.2013]
15. Egzamin: termin zerowy [12.06.2013]
16. Logiki atrybutowe i systemy regułowe.
17. Rozszerzenia logik klasycznych.

Materiały do wykładów - wersja robocza (.pdf)

Polecane materiały - e-learning

2. Rachunek predykatów I rzędu i Metoda Rezolucji (Google Preview) KRR: Ronald Brachman book
3. Rachunek predykatów I rzędu i Metoda Rezolucji KRR - slides

Zadanie dla ambitnych: korzystając z systemu Fitch udowodnić:

1. regułę rezolucji {ψ|p, φ|~p} |= {ψ|φ}
2. regułę rezolucji dualnej {ψ&φ} |= {ψ&p | φ&~p}

Plan ćwiczeń - 2014

1. Różne rozmaitości, czyli wprowadzenie do logiki w przededniu. Algebra zbiorów.
3. Rachunek zdań. Przekształcenia równoważne. Postacie CNF, DNF, NNF. Synteza układów logicznych.
4. Rachunek zdań. Dowodzenie twierdzeń.
6. Rachunek pierwszego rzędu. Dowodzenie. Rezolucja.

Sylabus

• Wprowadzenie do logiki, istota logiki, rola i zadania logiki, obszary zastosowań.
• Rola i znaczenie języka.
• Własności logiczne.
• Wywód. Pojęcie logicznej konsekwencji.
• Język rachunku zdań. Składnia i semantyka. Reguły przekształcania formuł. Postacie CNF, DNF, NNF. Reguły wnioskowania. Dowodzenie twierdzeń.
• Drzewa decyzyjne i diagramy OBDD.
• Logika rachunku predykatów. Składnia i semantyka. Reguły przekształcania formuł. Postacie CNF, DNF, NNF. Reguły wnioskowania. Dowodzenie twierdzeń.
• Logiki atrybutowe. Składnia i semantyka. Reguły przekształcania formuł. Postacie CNF, DNF, NNF. Reguły wnioskowania. Dowodzenie twierdzeń.
• Tablice i drzewa decyzyjne.
• Podstawy automatycznego dowodzenie twierdzeń. Reguła rezolucji. Reguła dualna. Podstawienia i unifikacja. Sprowadzanie do postaci normalnej. Strategie dowodzenia.
• Wstęp do programowania logicznego. Idea języka Prolog.
• Wybrane problemy i ograniczenia logiki klasycznej.
• Wybrane zastosowania i narzędzia logiki.
• Informacja o innych logikach.

Materiały pomocnicze