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. Logical consequence and logical equivalence. Transformations of formulas: equivalence transformation rules. Minterms and maxterms. Normal forms: CNF, DNF, NNF. Implicants and implicents. Maximal and minimal representation of CNF and DNF. What is the real meaning of CNF and DNF? [1.04.2020; ALi - on-line, via UPEL/ClickMeeting]
7. 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.
8. First -Order Logic. Syntax and Semantix. Logical transformation Rules. Logical inference rules. The Fitch system for FOPC.
9. CNF and DNF in FOPC. Transformations to S-form. Herbrand Base. Substituion and unification. Resolution in FOPC.
10. Introduction to logic programming. Prolog. Constraint Programming. Multi-valued logics. Fuzzy logic. Temporal and modal logics. Description logics.

Yet another chance:

On-line Logic Course - recommended

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

1. An Introduction to Logic
2. Propositional Calculus: Synatx, Sematics, Equivalence, CNF, DNF [ Support material for Lecture 6 : Czwartek, 2.04.2020, start godz. 12:00]
3. Propositional Calculus: Theorem Proving
4. Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT

1. Wprowadzenie do przedmiotu. Zasady pracy, zaliczenia, egzamin. Literatura. Elementarne wprowadzenie do logiki: język formalny, składnia, semantyka, wnioskowanie. Klasyfikacja problemów wnioskowania. Przykłady modelowania logicznego. Unicorn. [2.03.2018: ALi]
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).

1. Wprowadzenie do przedmiotu. Zasady pracy, zaliczenia, egzamin. Literatura. Elementarne wprowadzenie do logiki: język formalny, składnia, semantyka, wnioskowanie. Klasyfikacja problemów wnioskowania. Przykłady modelowania logicznego. Unicorn. [3.03.2017: ALi]
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.
8. Synteza układów logicznych. Tabele Karnaugha. Układy statyczne i dynamiczne. [28.04.2017]
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

1. Wprowadzenie do przedmiotu. Zasady pracy, zaliczenia, egzamin. Literatura. Elementarne wprowadzenie do logiki [26.02.2016: ALi]
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]

Materiały pomocnicze do wykładu:

Materiał uzupełniający

Logika-1: Wprowadzenie do logiki

Logika-2-3: Podstawy rachunku zdań

Logika-4: Dowodzenie w rachunku zdań

Logika-5-6: Elementy rachunku predykatów I rzędu

Podstawy syntezy układów logicznych

Wykład KJo 1 i 2

Wykład KJo zaawansowany

1. Elementarne wprowadzenie do logiki. Wprowadzenie do ćwiczeń. [4.03.2015]
2. Wprowadzenie do wykładu. Zasady pracy, zaliczenia, egzamin. Literatura. [11.03.2015]
3. Elementy podejścia systemowego: model, wejścia, wyjścia, cel. Zastosowania logiki. [18.03.2015]
4. Elementarne wprowadzenie do rachunku zdań. Wnioskowanie logiczne. Paradoksy. Przykłady. [25.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]

2015: Materiały do wykładów (robocze).

1. Logika 1-3
2. Logika 4-8
3. Logika 9
4. Logika 10
5. Logika 11-14

Wykłady - 2014

1. Elementarne wprowadzenie do logiki. Zasady pracy, zaliczenia, egzamin. Literatura. [5.03.2014]
2. Elementy podejścia systemowego: model, wejścia, wyjścia, cel. Zastosowania logiki. [12.03.2014]
3. Elementarne wprowadzenie do rachunku zdań. Wnioskowanie logiczne. Przykłady. [19.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)

1. logika-intro-1-3-2014

Polecane materiały - e-learning

1. Matryce logiczne - weryfikacja
2. http://kot.rogacz.com/Science/Studies/06/tpjp/wyklad/ [Polecam Wykład 1. Rachunek zdań]
3. Rachunek predykatów I rzędu i Metoda Rezolucji (Google Preview) KRR: Ronald Brachman book
4. Rachunek predykatów I rzędu i Metoda Rezolucji KRR - slides
5. Inne materiały na stronie Logika, Reprezentacja i przetwarzanie wiedzy, Prolog

Wykłady - 2013

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)

1. Wykłady 1-3
2. Wykłady 4-8
3. Wykład 9

Polecane materiały - e-learning

1. Matryce logiczne - weryfikacja
2. http://kot.rogacz.com/Science/Studies/06/tpjp/wyklad/ [Polecam Wykład 1. Rachunek zdań]
3. Rachunek predykatów I rzędu i Metoda Rezolucji (Google Preview) KRR: Ronald Brachman book
4. Rachunek predykatów I rzędu i Metoda Rezolucji KRR - slides
5. Inne materiały na stronie Logika, Reprezentacja i przetwarzanie wiedzy, Prolog

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.
2. Rachunek zdań. Podstawy. Składnia, semantyka, badanie własności formuł.
3. Rachunek zdań. Przekształcenia równoważne. Postacie CNF, DNF, NNF. Synteza układów logicznych.
4. Rachunek zdań. Dowodzenie twierdzeń.
5. Rachunek pierwszego rzędu. Składnia, semantyka, przykłady. Wprowadzenie do metody rezolucji.
6. Rachunek pierwszego rzędu. Dowodzenie. Rezolucja.

Sylabus

• Wprowadzenie do logiki, istota logiki, rola i zadania logiki, obszary zastosowań.
• Rola i znaczenie języka.
• Składnia, semantyka, interpretacja, model.
• Własności logiczne.
• Wywód. Pojęcie logicznej konsekwencji.
• Przykłady formalizacji problemów.
• 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

Linki

https://www.coursera.org/course/intrologic