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]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] 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. Przykłady wnioskowań. [8.11.2023; ALi] Propositional Calculus - … —- ====== Logika Matematyczna + Logic for Computer Science 2022/2023 lato/Summer====== —- - Introduction to Logic [7/9.03.2023;ALi] Introduction+Organization 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 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] 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] 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] 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: O szkodliwości nauczania logiki... Ciekawostka: Dlaczego Polska jest biedna... Zamiast komentarza do wykładu Warto przeczytać: ON SAT and SAT Solvers Warto zobaczyć: See how it works: A Simple DPLL SAT Solver ON-Line Warto zobaczyć: MiniSat in Your Browser Try an on-line tool: Logic calculator: Server-side Processing —- —- Archives: ====Logika Matematyczna/Logic for Computer Science 2021/2022==== - Introduction to Logic [1-2.03.2022;ALi] Introduction+Organization 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: Materiał uzupełniający Introduction+Organization - Introduction to Logic - Propositional Calculus: Syntax, Semantics, Logical Implication and Equivalence, CNF, DNF - Propositional Calculus: Introduction to Theorem Proving - Propositional Logic: SAT - First Order Predicate Calculus. Resolution. - Extensions: Multi-Valued, Fuzzy and Temporal Logics. - Description Logics - Algebra Boole'a, Synteza układów kombinacyjnych. —- Linki 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] Introduction+Organization - Podstawy logiki: Elementarne wprowadzenie do istoty logiki. Intuicyjne podstawy rachunku zdań. [14.10.2021;ALi] 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] 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: Materiał uzupełniający Introduction+Organization - Introduction to Logic - Propositional Calculus: Syntax, Semantics, Logical Implication and Equivalence, CNF, DNF - Propositional Calculus: Introduction to Theorem Proving - Propositional Logic: SAT - First Order Predicate Calculus. Resolution. - Extensions: Multi-Valued, Fuzzy and Temporal Logics. - Description Logics - Algebra Boole'a, Synteza układów kombinacyjnych. —- Linki 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] Introduction+Organization 1. Introduction to Logic - Introduction to Propositional Calculus [10.03.2021;ALi] - Propositional Logic. Functions, CNF, DNF. [17.03.2021;ALi] 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].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] 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] 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] Introduction to Logic (1) - Elementarne wprowadzenie do rachunku zdań. Składnia i semantyka. [9.10.2020; ALi] 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] 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] Propositional Calculus. Theorem Proving, Inference Rules. (3); 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] Propositional Calculus. Decision Trees and OBDD Diagrams. The SAT Problem (4) SAT Examples: DIMACS files (przykłady z wykładu) - Synteza układów logicznych. Tabele Karnaugha. Metoda Quine-McCluskey'a. [13.11.2020; ALi] 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]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. Kurs i materiały do Prologu Logiki deskrypcyjne. Logiki wielowartościowe i rozmyte. Logiki temporalne. [8.01.2021;ALi] Logiki Deskrypcyjne 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: 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: On-line Logic Course - recommended —- Rough lecture notes in .pdf (for cautious, personal use only): - An Introduction to Logic - Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF [ Support material for Lecture 3 : Czwartek, 2.04.2020, start godz. 12:00] - Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF [Update: 15-04-2020] - 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] - Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch [Update: 15-04-2020] - Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT - Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT [Update: 22/23-04-2020] - Predicate Calculus: Introduction, Syntax, Semantics. Variables, Terms, Quantifiers. Logical Formulas and their Interpretation [Update: 29/30-04-2020] - Predicate calculus: Syntax, Semantics, Herbrand Interpretation, Transformation Rules, Inference Rules, Resolution and Dual Resolution [Update: 6/7-05-2020] - Example of Resolution Proof: Marcus&Cesar - 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): * Omówienie CNF i DNF - test - 10 min (po polsku) | via MS Office OneDrive/AGH * Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF+examples (1.5h in English)| via MS Office OneDrive/AGH * Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch (1.5h in English)| via MS Office OneDrive/AGH * Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch (1.5h in Polish)| via MS Office OneDrive/AGH * Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT (1.5h in English)| via MS Office OneDrive/AGH) * Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT (1.5h in Polish via MS Office OneDrive/AGH) * 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) * 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) * 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) * 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) * Example of Resolution Proof: Marcus&Cesar 0.3h in Enlish via MS Office OneDrive/AGH (6.05.2020)) * Example of Resolution Proof: Marcus&Cesar 0.3h in Polish via MS Office OneDrive/AGH (7.05.2020)) * 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: 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 —- ==== 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). - Logika 1-3 - Logika 4-8 - Logika 9 - Logika 10 - 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) - logika-intro-1-3-2014 —- Polecane materiały - e-learning - 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) KRR: Ronald Brachman book - Rachunek predykatów I rzędu i Metoda Rezolucji KRR - slides - Inne materiały na stronie 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] - 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) - Wykłady 1-3 - Wykłady 4-8 - Wykład 9 Polecane materiały - e-learning - 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) KRR: Ronald Brachman book - Rachunek predykatów I rzędu i Metoda Rezolucji KRR - slides - Inne materiały na stronie 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