Both sides previous revision
Poprzednia wersja
Nowa wersja
|
Poprzednia wersja
|
pl:dydaktyka:logic:start [2020/03/24 21:34] ligeza [Logic for Computer Science: 2020] |
pl:dydaktyka:logic:start [2024/04/22 12:18] (aktualna) ligeza [Logika Matematyczna + Logic for Computer Science 2023/2024 lato/Summer] |
ψ | ψ |
====== Kurs z Logiki ====== | |
| |
| |
| |
| |
| |
| ====== Logika Matematyczna + Logic for Computer Science 2023/2024 lato/Summer====== |
| |
---- | ---- |
| |
| - **Introduction to Logic** [27/29.02.2024;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |1. Introduction to Logic}} |
| - **Introduction to Logic. Propositional Calculus.Syntax and Sematics** [5/7.03.2024;ALi]. |
| - **Propositional Calculus. Semantics. Logical implication and Equivalence. Maxterms and Minterms.CNF and DNF.** [12/14.03.2024;ALi] |
| - **Propositional Calculus. Intro to Theorem Proving. Theorem Proving Models. Resolution and Dual Resolution. Semantic Tableau.** [19/21.03.2024;ALi] |
| - **Theorem Proving. Resolution and Dual Resolution. Semantic Tableau. The Fitch System. Towards SAT.** [26.03/4.04.2024] |
| - **First-Order Predicate Calculus. Syntax, semantics, expressive power. Constants, variables, terms, predicates, quantifiers.** [9/11.04.2024] |
| - **First-Order Predicate Calculus. Theorem Proving. Resolution and Dual Resolution. A note on Multi-Valued, Fuzzy and Temporal Logics** [16/18.04.2024] |
| - <fc #ff00ff>Zero exam</fc> (CS only; June 2024) |
| |
| |
| |
| ---- |
| ---- |
| ---- |
| Support material for the Logic Lectures: |
| |
| {{:pl:dydaktyka:logic:wyklad1-kgd-2015.pdf|Materiał uzupełniający}} |
| |
| {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} |
| |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |Introduction to Logic}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_2.pdf |Propositional Calculus: Syntax, Semantics, Logical Implication and Equivalence, CNF, DNF}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_3.pdf |Propositional Calculus: Introduction to Theorem Proving}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_4.pdf |Propositional Logic: SAT}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_5.pdf |First Order Predicate Calculus. Resolution.}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_6.pdf |Extensions: Multi-Valued, Fuzzy and Temporal Logics.}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020_2021-7_dl_pl.pdf |Description Logics}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-bool-synt.pdf |Algebra Boole'a, Synteza układów kombinacyjnych.}} |
| |
| |
| ---- |
| |
| |
| __**Linki**__ |
| |
| [[https://www.coursera.org/course/intrologic|Polecany kurs Logiki — zapisz się i spróbuj swoich sił!]] |
| |
| [[http://intrologic.stanford.edu/public/chapters.php|Intrologic: Stanford]] |
| |
| ---- |
| |
| |
| ====== Logika dla Informatyków - ISI - 2023/2024-zima ====== |
| - **Inauguracja Roku Akademickiego w AGH.** [4.10.2023] |
| - **Wprowadzenie do kursu logiki. Sprawy organizacyjne i warunki zaliczenia. Motywacja i sylabus. Przykłady. Literatura i materiały pomocnicze. Dokumentacja kursu.** [11.10.2023; ALi]{{:pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} |
| - **Podstawy logiki: Elementarne wprowadzenie do istoty logiki. Język naturalny a język formalny. O potrzebie logiki. Paradoksy. Intuicyjne podstawy rachunku zdań. Dedukcja, Abdukcja i Indukcja. Przykłady formuł i reguł wnioskowania.** [18.10.2023;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |1. Introduction to Logic}} |
| - **Podstawy logiki. Składnia i semantyka rachunku zdań. Przykłady reguł wnioskowania. Logiczna konsekwencja, poprawność, spójność.** [25.10.2023;ALi] |
| - **Rachunek zdań: składnia i semantyka w ujęciu formalnym. Logiczna implikacja i równoważność. Tabele prawdy. Układy funkcjonalnie pełne. Transformacje zachowujące róẉnoważność.** [8.11.2023; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_2.pdf |Propositional Calculus}} |
| - **Rachunek zdań: składnia i semantyka w ujęciu formalnym. Transformacje zachowujące róẉnoważność. Weryfikacja tautologii i równoważności. Badanie logicznej konsekwencji. Postacie CNF i DNF. ** [15.11.2023; ALi] |
| - **CNF i DNF - dokończenie. Transformacje do CNF i DNF. Postacie minimalne i maksymalne. Zastosowania CNF i DNF. Notacje Sigma i Pi. Wprowadzenie do dowodzenia twierdzeń.** [22.11.2023; ALi] |
| - **Metody Dowodzenia Twierdzeń. Metoda Rezolucji i Rezolucji Dualnej. Semantic Tableau. System Fitcha. Przykłady.** [29.11.2023; ALi] |
| - **System Fitcha - przykłady. Wstęp do SAT. Wybrane narzędzia i przykłady: Unicorn, EX-LCV16, Tracing the Murder.** [6.12.2023; ALi] |
| -<fc #ff00ff> E-Learning: Wprowadzenie do Rachunku Predykatów (FOPC). Pojęcie predykatu. Relacje. Zmienne i termy. Kwantyfikatory.</fc> [13.12.2023; ALi] |
| - **Rachunek Predykatów (FOPC). Stałe, zmienne, termy. Predykaty, relacje, kwantyfikatory.** [20.12.2023; ALi] |
| - **FOPC. Składnia i Semantyka. ** [3.01.2024; ALi] |
| - <fc #00ff00>Logiczna konsekwencja i Równoważność. Wnioskowanie. Dowodzenie Twierdzeń.</fc> [10.01.2024; ALi] |
| - Metoda Rezolucji. Prolog. Rachunki nieklasyczne. Logiki opisowe. [17.01.2024; ALi] |
| |
| |
| |
| |
| |
| ---- |
| |
| ====== Logika Matematyczna + Logic for Computer Science 2022/2023 lato/Summer====== |
| |
| ---- |
| |
| - **Introduction to Logic** [7/9.03.2023;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |1. Introduction to Logic}} |
| - **Introduction to Propositional Calculus** [14/16.03.2023;ALi] |
| - **Propositional Calculus. Semantics. Logical implication and Equivalence. Maxterms and Minterms.CNF and DNF.** [21/23.03.2023;ALi] |
| - **Propositional Calculus. Intro to Theorem Proving. Theorem Proving. Resolution and Dual Resolution. Semantic Tableau. The Fitch System.** [28/30.03.2023;ALi] |
| - **Propositional Calculus. SAT.** [4/13.04.2023;ALi] |
| - **First-Order Predicate Calculus. Syntax, semantics, expressive power.** [18/20.04.2023; ALi] |
| - **First-Order Predicate Calculus. Theorem Proving. Resolution and Dual Resolution. A note on Multi-Valued, Fuzzy and Temporal Logics** [25/27.04.2023; ALi] |
| - Zero Exam (CS only: <fc #ff0000>16.06.2023, 17:00 on Upel</fc>). |
| |
| |
| ---- |
| ---- |
| =====Logika dla Informatyków: ISI - 2022-2023 (semestr zimowy; środy, sala H-24, B-1, godz. 13:15-14:45 ===== |
| |
| |
| __**Linki**__ |
| |
| [[https://www.coursera.org/course/intrologic|Polecany kurs Logiki — zapisz się i spróbuj swoich sił! Start: 5.10.2022]] |
| |
| https://www.coursera.org/learn/logic-introduction |
| |
| ---- |
| |
| - **Wprowadzenie do kursu logiki. Sprawy organizacyjne. Motywacja i sylabus. Przykłady. Literatura i materiały pomocnicze.** Dokumentacja kursu. [5.10.2022; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} |
| - **Podstawy logiki: Elementarne wprowadzenie do istoty logiki. Język naturalny a język formalny. O potrzebie logiki. Paradoksy. Intuicyjne podstawy rachunku zdań. Dedukcja, Abdukcja i Indukcja. Przykłady formuł i reguł wnioskowania** [12.10.2022;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |1. Introduction to Logic}} |
| - **Podstawy logiki. Składnia i semantyka rachunku zdań. Przykłady reguł wnioskowania. Logiczna konsekwencja, poprawność, spójność.** [19.10.2022;ALi] |
| - **Rachunek zdań: składnia i semantyka w ujęciu formalnym. Przykłady wnioskowań.** [26.10.2022; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_2.pdf |Propositional Calculus}} |
| - <fc #ff0000>**E-Learning: Rachunek zdań: składnia i semantyka w ujęciu formalnym. Logiczna implikacja i równoważność. Tabele prawdy. Układy funkcjonalnie pełne. Weryfikacja tautologii i równoważności. Transformacje zachowujące róẉnoważność.** [9.11.2022; ALi]</fc> |
| - **Rachunek zdań: składnia i semantyka w ujęciu formalnym. Logiczna implikacja i równoważność. Tabele prawdy. Układy funkcjonalnie pełne. Weryfikacja tautologii i równoważności. Transformacje zachowujące róẉnoważność.** [16.11.2022; ALi] |
| - **Rachunek zdań. Mintermy i makstermy; własności. Postacie CNF i DNF. Sprowadzanie do postaci CNF i DNF. Postacie minimalne i maksymalne.** [23.11.2022] |
| - **Rachunek zdań. Mintermy i makstermy; własności. Postacie CNF i DNF. Sprowadzanie do postaci CNF i DNF. Postacie minimalne i maksymalne. Zastosowania CNF i DNF. Notacje Sigma i Pi.** [30.11.2022] |
| -**Rachunek zdań. Wprowadzenie do dowodzenia twierdzeń.** [7.12.2022;ALi] |
| - **Rachunek zdań. Dowodzenie twierdzeń. Metoda Rezolucji i Rezolucji Dualnej. Semantic Tableau. System Fitcha.** [14.12.2022;ALi] |
| - **On-line. Rachunek zdań. Spełnialność i SAT.** [21.12.2022;ALi] |
| - **First Order Predicate Calculus (FOPC)** [4.01.2023] <fc #ff00ff>Uwaga: wykład w sali 429/C-2.</fc> |
| - **FOPC. Metoda Rezolucji. [11.01.2023]** <fc #ff00ff>Uwaga: wykład w sali 429/C-2.</fc> |
| - **FOPC. Metoda Rezolucji i Metoda Rezolucji Dualnej. Programowanie Logiczne. Język Prolog. Inne logiki.** [18.01.2023] <fc #ff00ff>Uwaga: wykład w sali 429/C-2.</fc> |
| |
| ---- |
| ---- |
| <fc #ff00ff>Ciekawostka:</fc> [[http://www.racjonalista.pl/kk.php/s,4416/q,O.szkodliwosci.logiki|O szkodliwości nauczania logiki...]] |
| |
| <fc #ff00ff>Ciekawostka:</fc> [[https://wiadomosci.wp.pl/kod-geniusza-jak-jaroslaw-duda-zmienil-swiat-i-nic-na-tym-nie-zarobil-6824682458536864a|Dlaczego Polska jest biedna... Zamiast komentarza do wykładu]] |
| |
| <fc #ff00ff>Warto przeczytać: </fc> [[https://www.borealisai.com/research-blogs/tutorial-9-sat-solvers-i-introduction-and-applications/|ON SAT and SAT Solvers]] |
| |
| |
| <fc #ff00ff>Warto zobaczyć: </fc>[[https://www.inf.ufpr.br/dpasqualin/d3-dpll/|See how it works: A Simple DPLL SAT Solver ON-Line]] |
| |
| <fc #ff00ff>Warto zobaczyć: </fc>[[https://www.msoos.org/2013/09/minisat-in-your-browser/|MiniSat in Your Browser]] |
| |
| <fc #ff00ff>Try an on-line tool:</fc> [[https://www.erpelstolz.at/gateway/formular-uk-zentral.html|Logic calculator: Server-side Processing]] |
| ---- |
| ---- |
| Archives: |
| |
| |
| ====Logika Matematyczna/Logic for Computer Science 2021/2022==== |
| |
| |
| - **Introduction to Logic** [1-2.03.2022;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |1. Introduction to Logic}} |
| - **Introduction to Propositional Calculus** [8-9.03.2022;ALi] |
| - **Propositional Calculus. Semantics. Logical implication and Equivalence. Maxterms and Minterms.** [15-16.03.2022;ALi] |
| - **Propositional Calculus. CNF and DNF. Intro to Theorem Proving.** [22-23.03.2022;ALi] |
| - **Propositional Calculus. Theorem Proving. Resolution and Dual Resolution. Semantic Tableau. The Fitch System.** [29-30.03.2022;ALi] |
| - **Propositional Calculus. SAT.** [5-6.04.2022;ALi] |
| - **First-Order Predicate Calculus. A note on Multi-Valued, Fuzzy and Temporal Logics** [12-13.04.2022; ALi] |
| |
| |
| ---- |
| ---- |
| Support material for the Logic Lectures: |
| |
| {{:pl:dydaktyka:logic:wyklad1-kgd-2015.pdf|Materiał uzupełniający}} |
| |
| {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} |
| |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |Introduction to Logic}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_2.pdf |Propositional Calculus: Syntax, Semantics, Logical Implication and Equivalence, CNF, DNF}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_3.pdf |Propositional Calculus: Introduction to Theorem Proving}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_4.pdf |Propositional Logic: SAT}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_5.pdf |First Order Predicate Calculus. Resolution.}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_6.pdf |Extensions: Multi-Valued, Fuzzy and Temporal Logics.}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020_2021-7_dl_pl.pdf |Description Logics}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-bool-synt.pdf |Algebra Boole'a, Synteza układów kombinacyjnych.}} |
| |
| |
| ---- |
| |
| |
| __**Linki**__ |
| |
| [[https://www.coursera.org/course/intrologic|Polecany kurs Logiki — zapisz się i spróbuj swoich sił! Start: 11.03.2022]] |
| |
| ---- |
| |
| =====Logika dla Informatyków: ISI - 2021-2022 (semestr zimowy; czwartki, sala 429 C-2, godz. 12:30-14:00 ===== |
| |
| - **Wprowadzenie do kursu logiki. Sprawy organizacyjne. Motywacja i sylabus. Przykłady. Literatura i materiały pomocnicze.** Dokumentacja kursu. [7.10.2021; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} |
| - **Podstawy logiki: Elementarne wprowadzenie do istoty logiki. Intuicyjne podstawy rachunku zdań.** [14.10.2021;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |1. Introduction to Logic}} |
| - **Podstawy logiki. Paradoksy. Składnia i semantyka rachunku zdań. Przykłady reguł wnioskowania. Logiczna konsekwencja, poprawność, spójność.** [21.10.2021;ALi] |
| - **Rachunek zdań: składnia i semantyka w ujęciu formalnym.** [28.10.2021; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_2.pdf |Propositional Calculus}} |
| - Rachunek zdań. Tabele prawdy. Układy funkcjonalnie pełne. Weryfikacja tautologii i równoważności. Logiczna konsekwencja. Transformacje równoważnościowe. Mintermy i Makstermy. [4.11.2021; ALi] |
| - [11.11.2021: <fc #008080>Święto Narodowe: Rocznica Odzyskania Niepodległości.</fc>]. |
| - **<fc #ff00ff>E-Learning: Rachunek zdań. Postacie CNF i DNF, Mintermy i makstermy. Sprowadzanie do postaci CNF i DNF. Postacie minimalne.</fc>** [18.11.2021; Individual study] |
| - **Rachunek zdań. Mintermy i makstermy; własności. Postacie CNF i DNF. Sprowadzanie do postaci CNF i DNF. Postacie minimalne i maksymalne.**[25.11.2021; ALi] |
| - **<fc #ff00ff>E-Learning: Rachunek zdań. Wprowadzenie do dowodzenia twierdzeń</fc>** (materiały: p. 3 - poniżej) [2.12.2021; Individual study] |
| - **<fc #ff00ff>E-Learning: Rachunek zdań. Wprowadzenie do dowodzenia twierdzeń</fc>** (materiały: p. 3 - poniżej) [9.12.2021; Individual study] |
| - Wykład na MS Teams 12:30-14:00 (kanał ogólny) [17.12.2021; ALi] - piątek! |
| - Wykład na MS Teams 12:30-14:00 (kanał ogólny) [22.12.2021; ALi] - środa! |
| - <fc #ff0000>Wykład na MS Teams 12:30-14:00 (kanał ogólny) [7.01.2022; ALi] - piątek!</fc> |
| - Wykład na MS Teams 12:30-14:00 (kanał ogólny) [14.01.2022; ALi] - piątek! |
| - Wykład na MS Teams 12:30-14:00 (kanał ogólny) [21.01.2022; ALi] - piątek! |
| |
| |
| ---- |
| ---- |
| Support material for the Logic Lectures: |
| |
| {{:pl:dydaktyka:logic:wyklad1-kgd-2015.pdf|Materiał uzupełniający}} |
| |
| {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} |
| |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |Introduction to Logic}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_2.pdf |Propositional Calculus: Syntax, Semantics, Logical Implication and Equivalence, CNF, DNF}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_3.pdf |Propositional Calculus: Introduction to Theorem Proving}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_4.pdf |Propositional Logic: SAT}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_5.pdf |First Order Predicate Calculus. Resolution.}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_6.pdf |Extensions: Multi-Valued, Fuzzy and Temporal Logics.}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020_2021-7_dl_pl.pdf |Description Logics}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-bool-synt.pdf |Algebra Boole'a, Synteza układów kombinacyjnych.}} |
| |
| |
| ---- |
| |
| |
| __**Linki**__ |
| |
| [[https://www.coursera.org/course/intrologic|Polecany kurs Logiki — zapisz się i spróbuj swoich sił! Start: 8.10.2021]] |
| |
| ---- |
| |
| ---- |
| ====Logika Matematyczna/Logic for Computer Science 2020/2021==== |
| |
| |
| - **Introduction to Logic** [3.03.2021;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_0.pdf |Introduction+Organization}} {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_1.pdf |1. Introduction to Logic}} |
| - **Introduction to Propositional Calculus** [10.03.2021;ALi] |
| - **Propositional Logic. Functions, CNF, DNF.** [17.03.2021;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_2.pdf |2. Propositional Logic: syntacs, semantics, logical equivalence, CNF, DNF.}} |
| - **Propositional Logic. Normal forms: CNF, CCNF, DNF, CDNF; implicants and implicents. Notations \Sigma and \Pi. Introduction to theorem proving.** [24.03.2021; ALi].{{ :pl:dydaktyka:logic:logic_for_computer_science_2021_3.pdf |3. Propositional Logic: Introduction to theorem Proving}} |
| - **Basic Theorem Proving in Propositional Calculus.** [31.03.2021; ALi] |
| - **Theorem Proving: Semantic Tableau, Fitch. SAT. CNF/DIMACS + SAT Solvers.** [14.04.2021;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2021_4.pdf |4. Propositiona Logic: SAT}} |
| - **First Order Predicate Calculus. Syntax and Semantics. Theorem Proving. Extension of the Fitch System. Resolution and Dual Resolution Theorem Proving.** [21.04.2021; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2020_2021_5.pdf |5. First Order Predicate Calculus. Resolution.}} |
| - Multi-Valued Logics. Fuzzy Logic. Temporal Logics. [28.04.2021; ALi] |
| ===== Logika dla Informatyków: ISI - 2020/2021 ===== |
| |
| - **Wprowadzenie do kursu. Wprowadzenie do istoty logiki. Przykłady.** [2.10.2020; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-1.pdf |Introduction to Logic (1)}} |
| - **Elementarne wprowadzenie do rachunku zdań. Składnia i semantyka.** [9.10.2020; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-2.pdf |Propositional Calculus (2)}} |
| - **Rachunek zdań. Tabele prawdy. Równoważność logiczna i implikacja logiczna. Nowe spójniki logiczne; funkcje logiczne. Systemy logiczne funkcjonalnie pełne. Przekształcenia równoważnościowe. Mintermy i makstermy. Postacie CNF i DNF. Implikanty i implicenty. Weryfikacja równoważności i logicznej implikacji formuł.** [16.10.2020; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-2.pdf |Propositional Calculus (2)}} |
| - **Rachunek zdań. Mintermy i makstermy. Postacie CNF i DNF. Implikanty i implicenty. Weryfikacja równoważności i logicznej implikacji formuł. Notacja Sigma i Pi. Wprowadzenie do dowodzenia w rachunku zdań. Pojęcie wywodu. Reguły wnioskowania. Metody dowodzenia twierdzeń.** [23.10.2020; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-3.pdf |Propositional Calculus. Theorem Proving, Inference Rules. (3)}}; {{ :pl:dydaktyka:logic:logic-links-23-10-2020.txt |Links to youtube for the lecture}} |
| - **Dowodzenie twierdzeń w rachunku zdań. Reguły, metody, strategie. Metoda Rezolucji i Rezolucji Dualnej. Metoda Semantic Tableau. System Fitcha.** [30.10.2020;ALi] |
| - **Analiza formuł rachunku zdań. Drzewa decyzyjne. Diagramy OBDD. Badanie spełnialności formuł: problem SAT.** [6.11.2020; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-4.pdf | Propositional Calculus. Decision Trees and OBDD Diagrams. The SAT Problem (4)}} {{ :pl:dydaktyka:logic:sat-minisat-examples.zip | SAT Examples: DIMACS files (przykłady z wykładu)}} |
| - **Synteza układów logicznych. Tabele Karnaugha. Metoda Quine-McCluskey'a.** [13.11.2020; ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-bool-synt.pdf |Algerbra Boole'a, Synteza układów kombinacyjnych.}} |
| - <fc #ff00ff>E-Learning: Rachunek predykatów I rzędu. Wprowadzenie. Składnia i semantyka. Reguły przekształceń równoważnościowych.</fc> [20.11.2020;ALi]{{ :pl:dydaktyka:logic:logic_for_computer_science_2020-5-fopc.pdf |Podstawy FOPC: Rachunek Predykatów I Rzędu}} |
| - **Rachunek predykatów I rzędu. Wprowadzenie. Składnia i semantyka.** [11.12.2020; ALi] |
| - **Rachunek predykatów I rzędu. Semantyka. Przekształcenia równoważnościowe. Reguły wnioskowania i dowodzenie twierdzeń. Metoda rezolucji. Metoda rezolucji dualnej.** [18.12.2020; ALi] |
| - **Wprowadzenie do programowania logicznego: Prolog. [[https://ai.ia.agh.edu.pl/pl:dydaktyka:pp:start|Kurs i materiały do Prologu]] Logiki deskrypcyjne. Logiki wielowartościowe i rozmyte. Logiki temporalne.** [8.01.2021;ALi] {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-dl-10.pdf |Logiki Deskrypcyjne}} {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-mvl-fl-tl.pdf |Logiki wielowartościowe, rozmyte i temporalne}} |
| |
| |
| |
| ---- |
| |
| |
===== Logic for Computer Science: 2020 ===== | ===== Logic for Computer Science: 2020 ===== |
| |
- **<fc #4682b4>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.</fc>** [18.03.2020 (online course; lecture 3 below)] | - **<fc #4682b4>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.</fc>** [18.03.2020 (online course; lecture 3 below)] |
- **<fc #4682b4>The role of CNF. The SAT problem. Approaches to solving the SAT problem. Decision trees. OBDD diagrams. SAT solvers.</fc>** [25.03.2020; lecture 4 below] | - **<fc #4682b4>The role of CNF. The SAT problem. Approaches to solving the SAT problem. Decision trees. OBDD diagrams. SAT solvers.</fc>** [25.03.2020; lecture 4 below] |
- 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. | - <fc #ff00ff>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?</fc> [Czwartek, 2.04.2020, 12:00-14:00; ALi - on-line, via UPEL/ClickMeeting] |
- First -Order Logic. Syntax and Semantix. Logical transformation Rules. Logical inference rules. The Fitch system for FOPC. | - <fc #ff00ff>Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch</fc> [Czwartek, 16.04.2020, 12:00-14:00; ALi - on-line, via UPEL/ClickMeeting] |
- CNF and DNF in FOPC. Transformations to S-form. Herbrand Base. Substituion and unification. Resolution in FOPC. | - <fc #ff00ff>Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT </fc> [Czwartek, 23.04.2020, 12:00-14:00; ALi - on-line, via UPEL/ClickMeeting] |
| - Boolean Algebra. Function syntehsis. The CNF and DNF again: the Pi and Sigma notations. Finding minimal representations. Logical circuits synthesis. Karnaugh Tables. The Quine-McCluskey algorithm. |
| - <fc #ff00ff>First-Order Logic. Variables, quantifiers, terms, predicates. Syntax and Semantix. Logical transformation Rules. Logical inference rules. The Fitch system for FOPC.</fc> [29/30.04.2020; ALi - online via UPEL] |
| - <fc #ff00ff>CNF and DNF in FOPC. Transformations to S-form. Herbrand Base. Substituion and unification. Resolution in FOPC. Dual Resolution. Examples.</fc> [6/7.05.2020; ALi - online via UPEL] |
- Introduction to logic programming. Prolog. Constraint Programming. Multi-valued logics. Fuzzy logic. Temporal and modal logics. Description logics. | - Introduction to logic programming. Prolog. Constraint Programming. Multi-valued logics. Fuzzy logic. Temporal and modal logics. Description logics. |
| |
| |
[[https://www.coursera.org/learn/logic-introduction|On-line Logic Course - recommended]] | [[https://www.coursera.org/learn/logic-introduction|On-line Logic Course - recommended]] |
| |
| |
| ---- |
| |
| |
Rough lecture notes in .pdf (for cautious, personal use only): | Rough lecture notes in .pdf (for cautious, personal use only): |
| |
- {{:pl:dydaktyka:logic:logic_for_computer_science_2020.pdf | An Introduction to Logic}} | - {{:pl:dydaktyka:logic:logic_for_computer_science_2020.pdf | An Introduction to Logic}} |
- {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-2.pdf | Propositional Calculus: Synatx, Sematics, Equivalence, CNF, DNF}} | - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-2.pdf | Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF }} [ <fc #ff00ff>Support material for Lecture 3</fc> : Czwartek, 2.04.2020, start godz. 12:00] |
- {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-3.pdf | Propositional Calculus: Theorem Proving}} | - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-prop-cal-2_15-04-2020.pdf | Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF}} [<fc #ff00ff>Update: 15-04-2020</fc>] |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-3.pdf | Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch}} [ <fc #ff00ff>Support material for Lecture 4</fc> : Czwartek, 16.04.2020, start godz. 12:00] |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-prop-proof-3_15-04-2020.pdf | Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch }} [<fc #ff00ff>Update: 15-04-2020</fc>] |
- {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-4.pdf | Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT}} | - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-4.pdf | Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT}} |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020_prop-sat-4-23-04-2020.pdf |Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT}} [<fc #ff00ff>Update: 22/23-04-2020</fc>] |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-fopc-29-04-2020.pdf |Predicate Calculus: Introduction, Syntax, Semantics. Variables, Terms, Quantifiers. Logical Formulas and their Interpretation}} [<fc #ff00ff>Update: 29/30-04-2020</fc>] |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-fopc-7-05-2020.pdf |Predicate calculus: Syntax, Semantics, Herbrand Interpretation, Transformation Rules, Inference Rules, Resolution and Dual Resolution}} [<fc #ff00ff>Update: 6/7-05-2020</fc>] |
| - [[https://aghedupl-my.sharepoint.com/:b:/g/personal/ligeza_agh_edu_pl/EZ2U8_hMxwBNvz3p0_k2Iq0BgvoxE0ji4rwoJ8FSI-TuNw?e=7d4hZf|Example of Resolution Proof: Marcus&Cesar]] |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-extras-14-05-2020.pdf |Multi-Valued Logics, Fuzzy Logic and Temporal Logics}} [<fc #ff00ff>Update: 14-05-2020</fc>] |
| |
| |
| ---- |
| |
| |
| |
| **__<fc #9400d3>New: Screencast from on-line lectures: video+sound (Use Google Chrome or try your browser):</fc>__** |
| |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EWOveLC-ghNIpJ_0bY0cuwMBwjCYH-N0uR5YCo_ngwauCQ?e=mCcVoL|Omówienie CNF i DNF - test - 10 min (po polsku) | via MS Office OneDrive/AGH]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EVlkWpYLU99Km70CgTtCjfEBiE85X1_4hB_4UKuE5ziAzQ?e=EBv795|Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF+examples (1.5h in English)| via MS Office OneDrive/AGH]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EdRc1zg3KiRJuyeIwiZ0cLMBaAqJOh6KFDLWwmen6VKRTw?e=HtJwJc|Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch (1.5h in English)| via MS Office OneDrive/AGH ]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/Eeuq3OyXKStKohoJt-pAJyUB-8gqlxoioZ2ggSHGfdCC0g?e=bzS6Nz|Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch (1.5h in Polish)| via MS Office OneDrive/AGH]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/Ef7gfKC56VBGoQuCj5_Gf5UBr2jBSW23xTdBhppK6V0o_A?e=6BkynT|Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT (1.5h in English)| via MS Office OneDrive/AGH)]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EZv11tm0Iy5JhVgh1Std8aIBObwX_-DH8JtY0PBccahf-Q?e=7bJILD|Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT (1.5h in Polish via MS Office OneDrive/AGH)]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EXbgXQekVgFIijlbgBrorXEBTXXiNxq9dra7PQmjblDW5A?e=DsfZ4V|Predicate Calculus: Introduction, Syntax, Semantics. Variables, Terms, Quantifiers. Logical Formulas and their Interpretation (1.5h in English via MS Office OneDrive/AGH (29.04.2020) ]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EbFyXe_7oFdAjrSLXrE-2FQB9SptBYxmJ2yfFlVGc4QO8A?e=VMnYJi|Predicate Calculus: Introduction, Syntax, Semantics. Variables, Terms, Quantifiers. Logical Formulas and their Interpretation (1.9h in Polish via MS Office OneDrive/AGH (30.04.2020)]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/Ee26uIEh_PdJlAnNLAg24WUB8iRRru0skOVddRWVI2-OIw?e=NfnW3I|Predicate calculus: Syntax, Semantics, Herbrand Interpretation, Transformation Rules, Inference Rules, Resolution and Dual Resolution (1.5h in English via MS Office OneDrive/AGH (6.05.2020) ]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EVP454rerYFOnzVFMa4qcUABk9SnJ7G_nFogczR3JqCm0Q?e=1eZgJ8|Predicate calculus: Syntax, Semantics, Herbrand Interpretation, Transformation Rules, Inference Rules, Resolution and Dual Resolution (1.7h in Polish via MS Office OneDrive/AGH (7.05.2020)]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EatvFBURWSxKnxCVvlZcBWYB-Y1F1fA7IHqZYl-xVwLJzA?e=nxdtsC|Example of Resolution Proof: Marcus&Cesar 0.3h in Enlish via MS Office OneDrive/AGH (6.05.2020))]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/EaDPClOgmDFKiM97zEVugPEBLkAZTtbwMdIDAsenf7DRGQ?e=3l51OI|Example of Resolution Proof: Marcus&Cesar 0.3h in Polish via MS Office OneDrive/AGH (7.05.2020))]] |
| * [[https://aghedupl-my.sharepoint.com/:v:/g/personal/ligeza_agh_edu_pl/ESJYibe6BnpDlS-GP4OLpPcB2DdDhktWga7Mt4jTtXs4xQ?e=ogyCEo|Multi-Valued Logics, Fuzzy Logic and Temporal Logics (0.5h in English via MS Office OneDrive/AGH (13.05.2020))]] |
| |
| |