ψ ====== 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] - Zero exam (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] - E-Learning: Wprowadzenie do Rachunku Predykatów (FOPC). Pojęcie predykatu. Relacje. Zmienne i termy. Kwantyfikatory. [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] - Logiczna konsekwencja i Równoważność. Wnioskowanie. Dowodzenie Twierdzeń. [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: 16.06.2023, 17:00 on Upel). ---- ---- =====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}} - **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] - **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] Uwaga: wykład w sali 429/C-2. - **FOPC. Metoda Rezolucji. [11.01.2023]** Uwaga: wykład w sali 429/C-2. - **FOPC. Metoda Rezolucji i Metoda Rezolucji Dualnej. Programowanie Logiczne. Język Prolog. Inne logiki.** [18.01.2023] Uwaga: wykład w sali 429/C-2. ---- ---- Ciekawostka: [[http://www.racjonalista.pl/kk.php/s,4416/q,O.szkodliwosci.logiki|O szkodliwości nauczania logiki...]] Ciekawostka: [[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]] Warto przeczytać: [[https://www.borealisai.com/research-blogs/tutorial-9-sat-solvers-i-introduction-and-applications/|ON SAT and SAT Solvers]] Warto zobaczyć: [[https://www.inf.ufpr.br/dpasqualin/d3-dpll/|See how it works: A Simple DPLL SAT Solver ON-Line]] Warto zobaczyć: [[https://www.msoos.org/2013/09/minisat-in-your-browser/|MiniSat in Your Browser]] Try an on-line tool: [[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: Święto Narodowe: Rocznica Odzyskania Niepodległości.]. - **E-Learning: Rachunek zdań. Postacie CNF i DNF, Mintermy i makstermy. Sprowadzanie do postaci CNF i DNF. Postacie minimalne.** [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] - **E-Learning: Rachunek zdań. Wprowadzenie do dowodzenia twierdzeń** (materiały: p. 3 - poniżej) [2.12.2021; Individual study] - **E-Learning: Rachunek zdań. Wprowadzenie do dowodzenia twierdzeń** (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! - Wykład na MS Teams 12:30-14:00 (kanał ogólny) [7.01.2022; ALi] - piątek! - 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.}} - E-Learning: Rachunek predykatów I rzędu. Wprowadzenie. Składnia i semantyka. Reguły przekształceń równoważnościowych. [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 ===== - **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] - **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: [[https://www.agh.edu.pl/aktualnosci/info/article/agh-zawiesza-zajecia-dydaktyczne/|AGH - Decision/Decycja]]** We switch to asynchronous, on-line course. Topics, dates, and selection of material are presented in **steel-blue**. - **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)] - **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)] - **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] - 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? [Czwartek, 2.04.2020, 12:00-14:00; ALi - on-line, via UPEL/ClickMeeting] - Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch [Czwartek, 16.04.2020, 12:00-14:00; ALi - on-line, via UPEL/ClickMeeting] - Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT [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. - First-Order Logic. Variables, quantifiers, terms, predicates. Syntax and Semantix. Logical transformation Rules. Logical inference rules. The Fitch system for FOPC. [29/30.04.2020; ALi - online via UPEL] - CNF and DNF in FOPC. Transformations to S-form. Herbrand Base. Substituion and unification. Resolution in FOPC. Dual Resolution. Examples. [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. Yet another chance: [[https://www.coursera.org/learn/logic-introduction|On-line Logic Course - recommended]] ---- 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-2.pdf | Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF }} [ Support material for Lecture 3 : Czwartek, 2.04.2020, start godz. 12:00] - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-prop-cal-2_15-04-2020.pdf | Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF}} [Update: 15-04-2020] - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-3.pdf | Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch}} [ Support material for Lecture 4 : 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 }} [Update: 15-04-2020] - {{ :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}} [Update: 22/23-04-2020] - {{ :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}} [Update: 29/30-04-2020] - {{ :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}} [Update: 6/7-05-2020] - [[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}} [Update: 14-05-2020] ---- **__New: Screencast from on-line lectures: video+sound (Use Google Chrome or try your browser):__** * [[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))]] ===== Plan wykładu z logiki: 2018 ===== - **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] - **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] -**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] - **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] - [30.03.2018 - wolne na Święta: Wielkanoc!] - //E-learning: wyznaczyć implikanty i implcenty dla modelu Unicorn.// [6.04.2018; ALi] - **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] - **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] - **Synteza układów logicznych.Implikanty i implicenty: minimalizacja funkcji. Tabele Karnaugha. Metoda Quine'a-McCluskey. Układy statyczne i dynamiczne.** [27.04.2018] - **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] - //Juwenalia - godziny rektorskie// [18.05.2018] - 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] - 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 ===== - **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] - **Wprowadzenie do rachunku zdań (Propositional Calculus). Składnia, semantyka. Pojęcie interpretacji i logicznej konsekwencji. Równoważność logiczna formuł.** [10.03.2017: ALi] - **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] - **Postacie CNF, DNF, NNF. Interpretacja postaci CNF i DNF. Zastosowania. Reguły wnioskowania. Metody dowodzenia w rachunku zdań.** [24.03.2017;ALi] - **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] - **Wybrane zaawansowane zagadnienia KRZ. Systemy Hilberta.** [7.04.2017] [KJo] - [21.04.2017] E-Learning. - **Synteza układów logicznych. Tabele Karnaugha. Układy statyczne i dynamiczne.** [28.04.2017] - **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] - Logika Juwenaliów [12.05.2017: godziny rektorskie]. - 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. - 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==== - **Wprowadzenie do przedmiotu. Zasady pracy, zaliczenia, egzamin. Literatura. Elementarne wprowadzenie do logiki** [26.02.2016: ALi] - **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] - **Wstęp do aksjomatycznego ujęcia KRZ i dowodów metodą aksjomatyczną; twierdzenie o dedukcji.** [11.03.2016; KJo] - **Aksjomatyczne ujęcie KRZ-kontynuacja; KRZ w ujęciu metalogicznym (twierdzenie o pełności, zwartości, niesprzeczności).** [18.03.2016; KJo] - **Postacie CNF, DNF, NNF. Reguły wnioskowania. Metody dowodzenia w rachunku zdań.** [1.04.2016; ALi] - **Metoda rezolucji i jej zastosowania. Metoda rezolucji dualnej. Semantic Tableau. System Fitcha.** [8.04.2016: ALi] - **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] - **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] - **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] - **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: {{:pl:dydaktyka:logic:wyklad1-kgd-2015.pdf|Materiał uzupełniający}} {{:pl:dydaktyka:logic:logika-1_2016.pdf|Logika-1: Wprowadzenie do logiki}} {{:pl:dydaktyka:logic:logika-2-3_2016.pdf|Logika-2-3: Podstawy rachunku zdań}} {{:pl:dydaktyka:logic:logika-4_2016.pdf|Logika-4: Dowodzenie w rachunku zdań}} {{:pl:dydaktyka:logic:logika-5-6_2016.pdf|Logika-5-6: Elementy rachunku predykatów I rzędu}} {{:pl:dydaktyka:logic:logika-boole-synthesis-9.pdf|Podstawy syntezy układów logicznych}} ---- {{:pl:dydaktyka:logic:logikawykladyuzup..pdf|Wykład KJo 1 i 2}} {{:pl:dydaktyka:logic:krakowwyklad1.pdf|Wykład KJo zaawansowany}} ---- ==== Wykłady - 2015 ==== - **Elementarne wprowadzenie do logiki. Wprowadzenie do ćwiczeń. ** [4.03.2015] - **Wprowadzenie do wykładu. Zasady pracy, zaliczenia, egzamin. Literatura. ** [11.03.2015] - **Elementy podejścia systemowego: model, wejścia, wyjścia, cel. Zastosowania logiki. ** [18.03.2015] - **Elementarne wprowadzenie do rachunku zdań. Wnioskowanie logiczne. Paradoksy. Przykłady. ** [25.03.2015] - **Składnia i semantyka rachunku zdań. Interpretacje i modele. Równoważność. Przykłady modeli logicznych. ** [1.04.2015] - **Interpretacja formuł rachunku zdań. Tabele prawdy. Równoważność i wynikanie. Definicje spójników. Systemy funkcjonalnie pełne. ** [8.04.2015] - **Weryfikacja tautologii i konsekwencji logicznej w oparciu o tabele prawdy. Mintermy i makstermy. Klauzule Horna. ** [15.04.2015] - **Postacie CNF, DNF i NNF i ich znaczenie. Sprowadzanie formuły do CNF, DNF i NNF. Implikanty i implicenty. ** [22.04.2015] - **Reguły wnioskowania. Metody dowodzenia twierdzeń. Twierdzenia o dedukcji. Przykłady. ** [29.04.2015] - **Rezolucja i rezolucja dualna. Zbiór logicznych konsekwencji. Metoda tablic semantycznych. Systemy Gentzenowskie. Drzewa decyzyjne. Diagramy OBDD.**[6.05.2015] - Rachunek predykatów I rzędu.Składnia i semantyka [13.05.2015] - Rachunek predykatów I rzędu. Postacie CNF, DNF, NNF. Reguły przekształceń formuł z kwantyfikatorami. [27.05.2015] - Rachunek predykatów I rzędu. Podstawienia, unifikacja i rezolucja. [3.06.2015] - Zastosowania logiki. Język Prolog. Przykłady programów logicznych. Logiki nieklasyczne. [10.06.2015] ---- 2015: Materiały do wykładów (robocze). - {{:pl:dydaktyka:logic:logika-intro-1-3-2014.pdf|Logika 1-3}} - {{:pl:dydaktyka:logic:logika-propositional-calculus-4-8-zmienione-new.pdf|Logika 4-8}} - {{:pl:dydaktyka:logic:logika-boole-synthesis-9.pdf|Logika 9}} - {{:pl:dydaktyka:logic:logika-propositional-calculus-10-2015.pdf|Logika 10}} - {{:pl:dydaktyka:logic:logika-kwantyfikatory-11-14-dl.pdf|Logika 11-14}} ---- ---- ---- __**Wykłady - 2014**__ - **Elementarne wprowadzenie do logiki. Zasady pracy, zaliczenia, egzamin. Literatura. ** [5.03.2014] - **Elementy podejścia systemowego: model, wejścia, wyjścia, cel. Zastosowania logiki. ** [12.03.2014] - **Elementarne wprowadzenie do rachunku zdań. Wnioskowanie logiczne. Przykłady. ** [19.03.2014] - **Składnia i semantyka rachunku zdań. Równoważność logiczna a logiczna konsekwencja. Przykłady modeli logicznych. ** [26.03.2014] - **Interpretacja formuł rachunku zdań. Tabele prawdy. Równoważność i wynikanie. Definicje spójników. Systemy funkcjonalnie pełne. ** [2.04.2014] - **Weryfikacja tautologii i konsekwencji logicznej w oparciu o tabele prawdy. Mintermy i makstermy. Klauzule Horna. ** [9.04.2014; K.G-D] - **Postacie CNF, DNF i NNF i ich znaczenie. Sprowadzanie formuły do CNF, DNF i NNF. Implikanty i implicenty. ** [16.04.2014] - **Algebra Boole'a. Funkcje Boolowskie. Synteza układów. Bramki logiczne. Tablice Karnaugha. ** [23.04.2014] - **Reguły wnioskowania. Metody dowodzenia twierdzeń. Twierdzenia o dedukcji. Przykłady. ** [30.04.2014] - **Rezolucja i rezolucja dualna. Zbiór logicznych konsekwencji. Tablice Karnaugha, sklejanie, minimalizacja. Metoda Quine-McCluskey'a. **[7.05.2014] - **Drzewa decyzyjne. Diagramy OBDD. Metoda tablic semantycznych. Dedukcja naturalna.** [14.05.2014]. - **Rachunek predykatów I rzędu.Składnia i semantyka** [21.05.2014] - **Rachunek predykatów I rzędu. Postacie CNF, DNF, NNF. Reguły przekształceń formuł z kwantyfikatorami.** [28.05.2014] - **Rachunek predykatów I rzędu. Podstawienia, unifikacja i rezolucja.** [4.06.2014] - **Zastosowania logiki. Język Prolog. Przykłady programów logicznych. Logiki nieklasyczne.** [11.06.2014] ---- __**Materiały do wykładów - wersja robocza (.pdf)**__ - {{:pl:dydaktyka:logic:logika-intro-1-3-2014.pdf|logika-intro-1-3-2014}} ---- __**Polecane materiały - e-learning**__ - [[http://robert.nowotniak.com/pl/artificial-intelligence/tautolog/|Matryce logiczne - weryfikacja]] - [[http://kot.rogacz.com/Science/Studies/06/tpjp/wyklad/]] [Polecam Wykład 1. Rachunek zdań] - Rachunek predykatów I rzędu i Metoda Rezolucji (Google Preview) [[http://store.elsevier.co/product.jsp?isbn=9781558609327 | KRR: Ronald Brachman book]] - Rachunek predykatów I rzędu i Metoda Rezolucji [[http://www.cs.toronto.edu/~hector/PublicKRSlides.pdf | KRR - slides]] - Inne materiały na stronie [[http://ai.ia.agh.edu.pl/wiki/pl:dydaktyka:krr:start | Logika, Reprezentacja i przetwarzanie wiedzy, Prolog]] ---- ---- __**Wykłady - 2013**__ - **Wprowadzenie do logiki. E-learning.** [27.02.2013] - **Elementy logiki w ujęciu systemowym.** [6.03.2013] - **Podstawowe koncepcje logiki. Składnia. Semantyka. Wnioskowania.** [13.03.2013] - **Rachunek zdań. Składnia. Semantyka. Logiczna konsekwencja. Równoważność.** [20.03.2013] - **Rachunek zdań. Funkcje logiczne. Systemy funkcjonalnie pełne. Transformacje zachowujące równoważność.** [27.03.2013] - [[https://class.coursera.org/intrologic-003/auth/welcome?type=logout&visiting=https%3A%2F%2Fclass.coursera.org%2Fintrologic-003%2Fclass%2Findex | Logic Course at Stanford]] [3.04.2013 - e-learning] - **Rachunek zdań. Postacie CNF, DNF, NNF.** [10.04.2013] - **Reguły wnioskowania. Wywód. Dowodzenie twierdzeń. Rezolucja. Rezolucja dualna.** [17.04.2013] - **Algebra Boole'a. Minimalizacja funkcji logicznych. Tablice Karnaugha. Algorytm Quine'a-McCluskeya.** [24.04.2013]. - **E-learning:** __Rachunek zdań. Powtórzenie, usystematyzowanie i uzupełnienie wiadomości__ [8.05.2013] - **Drzewa decyzyjne. Diagramy OBDD. Metoda tablic semantycznych. Dedukcja naturalna.** [15.05.2013]. - **Rachunek predykatów I rzędu.** [22.05.2013] - **E-learning:** __Metoda rezolucji.__ [29.05.2013] - __Metoda Rezolucji. Metoda rezolucji dualnej. Prolog i programowanie w logice. Ograniczenia logik klasycznych. Logiki nieklasyczne. __ [5.06.2013] - __Egzamin: termin zerowy__ [12.06.2013] - Logiki atrybutowe i systemy regułowe. - Rozszerzenia logik klasycznych. __**Materiały do wykładów - wersja robocza (.pdf)**__ - {{:pl:dydaktyka:logic:logika-intro-1-3.pdf|Wykłady 1-3}} - {{:pl:dydaktyka:logic:logika-propositional-calculus-4-8.pdf|Wykłady 4-8}} - {{:pl:dydaktyka:logic:logika-boole-synthesis-9.pdf|Wykład 9}} __**Polecane materiały - e-learning**__ - [[http://robert.nowotniak.com/pl/artificial-intelligence/tautolog/|Matryce logiczne - weryfikacja]] - [[http://kot.rogacz.com/Science/Studies/06/tpjp/wyklad/]] [Polecam Wykład 1. Rachunek zdań] - Rachunek predykatów I rzędu i Metoda Rezolucji (Google Preview) [[http://store.elsevier.co/product.jsp?isbn=9781558609327 | KRR: Ronald Brachman book]] - Rachunek predykatów I rzędu i Metoda Rezolucji [[http://www.cs.toronto.edu/~hector/PublicKRSlides.pdf | KRR - slides]] - Inne materiały na stronie [[http://ai.ia.agh.edu.pl/wiki/pl:dydaktyka:krr:start | Logika, Reprezentacja i przetwarzanie wiedzy, Prolog]] Zadanie dla ambitnych: korzystając z systemu Fitch udowodnić: - regułę rezolucji {ψ|p, φ|~p} |= {ψ|φ} - regułę rezolucji dualnej {ψ&φ} |= {ψ&p | φ&~p} ---- __**Plan ćwiczeń - 2014**__ - Różne rozmaitości, czyli wprowadzenie do logiki w przededniu. Algebra zbiorów. - Rachunek zdań. Podstawy. Składnia, semantyka, badanie własności formuł. - Rachunek zdań. Przekształcenia równoważne. Postacie CNF, DNF, NNF. Synteza układów logicznych. - Rachunek zdań. Dowodzenie twierdzeń. - Rachunek pierwszego rzędu. Składnia, semantyka, przykłady. Wprowadzenie do metody rezolucji. - 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]]