1. Introduction to Logic [27/29.02.2024;ALi] Introduction+Organization 1. Introduction to Logic
2. Introduction to Logic. Propositional Calculus.Syntax and Sematics [5/7.03.2024;ALi].
3. Propositional Calculus. Semantics. Logical implication and Equivalence. Maxterms and Minterms.CNF and DNF. [12/14.03.2024;ALi]
4. Propositional Calculus. Intro to Theorem Proving. Theorem Proving Models. Resolution and Dual Resolution. Semantic Tableau. [19/21.03.2024;ALi]
5. Theorem Proving. Resolution and Dual Resolution. Semantic Tableau. The Fitch System. Towards SAT. [26.03/4.04.2024]
6. First-Order Predicate Calculus. Syntax, semantics, expressive power. Constants, variables, terms, predicates, quantifiers. [9/11.04.2024]
7. First-Order Predicate Calculus. Theorem Proving. Resolution and Dual Resolution. A note on Multi-Valued, Fuzzy and Temporal Logics [16/18.04.2024]
8. Zero exam (CS only; June 2024)

Support material for the Logic Lectures:

Materiał uzupełniający

Introduction+Organization

1. Introduction to Logic
2. Propositional Calculus: Syntax, Semantics, Logical Implication and Equivalence, CNF, DNF
3. Propositional Calculus: Introduction to Theorem Proving
4. Propositional Logic: SAT
5. First Order Predicate Calculus. Resolution.
6. Extensions: Multi-Valued, Fuzzy and Temporal Logics.
7. Description Logics
8. Algebra Boole'a, Synteza układów kombinacyjnych.

Linki

Polecany kurs Logiki — zapisz się i spróbuj swoich sił!

Intrologic: Stanford

1. Inauguracja Roku Akademickiego w AGH. [4.10.2023]
2. 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
3. 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
4. Podstawy logiki. Składnia i semantyka rachunku zdań. Przykłady reguł wnioskowania. Logiczna konsekwencja, poprawność, spójność. [25.10.2023;ALi]
5. 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] Propositional Calculus
6. 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]
7. 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]
8. Metody Dowodzenia Twierdzeń. Metoda Rezolucji i Rezolucji Dualnej. Semantic Tableau. System Fitcha. Przykłady. [29.11.2023; ALi]
9. System Fitcha - przykłady. Wstęp do SAT. Wybrane narzędzia i przykłady: Unicorn, EX-LCV16, Tracing the Murder. [6.12.2023; ALi]
10. E-Learning: Wprowadzenie do Rachunku Predykatów (FOPC). Pojęcie predykatu. Relacje. Zmienne i termy. Kwantyfikatory. [13.12.2023; ALi]
11. Rachunek Predykatów (FOPC). Stałe, zmienne, termy. Predykaty, relacje, kwantyfikatory. [20.12.2023; ALi]
12. FOPC. Składnia i Semantyka. [3.01.2024; ALi]
13. Logiczna konsekwencja i Równoważność. Wnioskowanie. Dowodzenie Twierdzeń. [10.01.2024; ALi]
14. Metoda Rezolucji. Prolog. Rachunki nieklasyczne. Logiki opisowe. [17.01.2024; ALi]

1. Introduction to Logic [7/9.03.2023;ALi] Introduction+Organization 1. Introduction to Logic
2. Introduction to Propositional Calculus [14/16.03.2023;ALi]
3. Propositional Calculus. Semantics. Logical implication and Equivalence. Maxterms and Minterms.CNF and DNF. [21/23.03.2023;ALi]
4. Propositional Calculus. Intro to Theorem Proving. Theorem Proving. Resolution and Dual Resolution. Semantic Tableau. The Fitch System. [28/30.03.2023;ALi]
5. Propositional Calculus. SAT. [4/13.04.2023;ALi]
6. First-Order Predicate Calculus. Syntax, semantics, expressive power. [18/20.04.2023; ALi]
7. First-Order Predicate Calculus. Theorem Proving. Resolution and Dual Resolution. A note on Multi-Valued, Fuzzy and Temporal Logics [25/27.04.2023; ALi]
8. Zero Exam (CS only: 16.06.2023, 17:00 on Upel).

Linki

Polecany kurs Logiki — zapisz się i spróbuj swoich sił! Start: 5.10.2022

https://www.coursera.org/learn/logic-introduction

1. Wprowadzenie do kursu logiki. Sprawy organizacyjne. Motywacja i sylabus. Przykłady. Literatura i materiały pomocnicze. Dokumentacja kursu. [5.10.2022; ALi] Introduction+Organization
2. 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
3. Podstawy logiki. Składnia i semantyka rachunku zdań. Przykłady reguł wnioskowania. Logiczna konsekwencja, poprawność, spójność. [19.10.2022;ALi]
4. Rachunek zdań: składnia i semantyka w ujęciu formalnym. Przykłady wnioskowań. [26.10.2022; ALi] Propositional Calculus
5. 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]
6. 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]
7. 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]
8. 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]
9. Rachunek zdań. Wprowadzenie do dowodzenia twierdzeń. [7.12.2022;ALi]
10. Rachunek zdań. Dowodzenie twierdzeń. Metoda Rezolucji i Rezolucji Dualnej. Semantic Tableau. System Fitcha. [14.12.2022;ALi]
11. On-line. Rachunek zdań. Spełnialność i SAT. [21.12.2022;ALi]
12. First Order Predicate Calculus (FOPC) [4.01.2023] Uwaga: wykład w sali 429/C-2.
13. FOPC. Metoda Rezolucji. [11.01.2023] Uwaga: wykład w sali 429/C-2.
14. 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:

1. Introduction to Logic [1-2.03.2022;ALi] Introduction+Organization 1. Introduction to Logic
2. Introduction to Propositional Calculus [8-9.03.2022;ALi]
3. Propositional Calculus. Semantics. Logical implication and Equivalence. Maxterms and Minterms. [15-16.03.2022;ALi]
4. Propositional Calculus. CNF and DNF. Intro to Theorem Proving. [22-23.03.2022;ALi]
5. Propositional Calculus. Theorem Proving. Resolution and Dual Resolution. Semantic Tableau. The Fitch System. [29-30.03.2022;ALi]
6. Propositional Calculus. SAT. [5-6.04.2022;ALi]
7. 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

1. Introduction to Logic
2. Propositional Calculus: Syntax, Semantics, Logical Implication and Equivalence, CNF, DNF
3. Propositional Calculus: Introduction to Theorem Proving
4. Propositional Logic: SAT
5. First Order Predicate Calculus. Resolution.
6. Extensions: Multi-Valued, Fuzzy and Temporal Logics.
7. Description Logics
8. Algebra Boole'a, Synteza układów kombinacyjnych.

Linki

Polecany kurs Logiki — zapisz się i spróbuj swoich sił! Start: 11.03.2022

1. Wprowadzenie do kursu logiki. Sprawy organizacyjne. Motywacja i sylabus. Przykłady. Literatura i materiały pomocnicze. Dokumentacja kursu. [7.10.2021; ALi] Introduction+Organization
2. Podstawy logiki: Elementarne wprowadzenie do istoty logiki. Intuicyjne podstawy rachunku zdań. [14.10.2021;ALi] 1. Introduction to Logic
3. Podstawy logiki. Paradoksy. Składnia i semantyka rachunku zdań. Przykłady reguł wnioskowania. Logiczna konsekwencja, poprawność, spójność. [21.10.2021;ALi]
4. Rachunek zdań: składnia i semantyka w ujęciu formalnym. [28.10.2021; ALi] Propositional Calculus
5. 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]
6. [11.11.2021: Święto Narodowe: Rocznica Odzyskania Niepodległości.].
7. E-Learning: Rachunek zdań. Postacie CNF i DNF, Mintermy i makstermy. Sprowadzanie do postaci CNF i DNF. Postacie minimalne. [18.11.2021; Individual study]
8. 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]
9. E-Learning: Rachunek zdań. Wprowadzenie do dowodzenia twierdzeń (materiały: p. 3 - poniżej) [2.12.2021; Individual study]
10. E-Learning: Rachunek zdań. Wprowadzenie do dowodzenia twierdzeń (materiały: p. 3 - poniżej) [9.12.2021; Individual study]
11. Wykład na MS Teams 12:30-14:00 (kanał ogólny) [17.12.2021; ALi] - piątek!
12. Wykład na MS Teams 12:30-14:00 (kanał ogólny) [22.12.2021; ALi] - środa!
13. Wykład na MS Teams 12:30-14:00 (kanał ogólny) [7.01.2022; ALi] - piątek!
14. Wykład na MS Teams 12:30-14:00 (kanał ogólny) [14.01.2022; ALi] - piątek!
15. 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

1. Introduction to Logic
2. Propositional Calculus: Syntax, Semantics, Logical Implication and Equivalence, CNF, DNF
3. Propositional Calculus: Introduction to Theorem Proving
4. Propositional Logic: SAT
5. First Order Predicate Calculus. Resolution.
6. Extensions: Multi-Valued, Fuzzy and Temporal Logics.
7. Description Logics
8. Algebra Boole'a, Synteza układów kombinacyjnych.

Linki

Polecany kurs Logiki — zapisz się i spróbuj swoich sił! Start: 8.10.2021

1. Introduction to Logic [3.03.2021;ALi] Introduction+Organization 1. Introduction to Logic
2. Introduction to Propositional Calculus [10.03.2021;ALi]
3. Propositional Logic. Functions, CNF, DNF. [17.03.2021;ALi] 2. Propositional Logic: syntacs, semantics, logical equivalence, CNF, DNF.
4. 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
5. Basic Theorem Proving in Propositional Calculus. [31.03.2021; ALi]
6. Theorem Proving: Semantic Tableau, Fitch. SAT. CNF/DIMACS + SAT Solvers. [14.04.2021;ALi] 4. Propositiona Logic: SAT
7. 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.
8. Multi-Valued Logics. Fuzzy Logic. Temporal Logics. [28.04.2021; ALi]

1. Wprowadzenie do kursu. Wprowadzenie do istoty logiki. Przykłady. [2.10.2020; ALi] Introduction to Logic (1)
2. Elementarne wprowadzenie do rachunku zdań. Składnia i semantyka. [9.10.2020; ALi] Propositional Calculus (2)
3. 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)
4. 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
5. Dowodzenie twierdzeń w rachunku zdań. Reguły, metody, strategie. Metoda Rezolucji i Rezolucji Dualnej. Metoda Semantic Tableau. System Fitcha. [30.10.2020;ALi]
6. 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)
7. Synteza układów logicznych. Tabele Karnaugha. Metoda Quine-McCluskey'a. [13.11.2020; ALi] Algerbra Boole'a, Synteza układów kombinacyjnych.
8. 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
9. Rachunek predykatów I rzędu. Wprowadzenie. Składnia i semantyka. [11.12.2020; ALi]
10. 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]
11. 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

1. Introduction to the Course. Goals and principles. Introduction to Logic. Basics of Propositional Calculus. Example syntax and a note on interpretation/semantics. Example inference rules. Elements of Big Picture. Examples of problems and their solutions. [26.02.2020; ALi]
2. Propositional Calculus. Syntax and Sematics. Logical consequence and logical equivalence. Truth tables and their analysis. Selected Boolean Functions. Functional Completeness. Properties of logical formulas. [4.03.2020; ALi]
   Uwaga: Zajęcia odwołane 11.03.2020 godz. 10:00 do 24/25(?).03.2020! Attention: Lectures/classes cancelled until March 24/25-th(?), 2020! See: AGH - Decision/Decycja We switch to asynchronous, on-line course. Topics, dates, and selection of material are presented in steel-blue.
3. Logical equivalence. Transformations of formulas: equivalent transformation rules. Minterms and maxterms. Normal forms: CNF, DNF, NNF. Implicants and implicents. Minimal representation. [11.03.2020 (online course; lecture 2 below)]
4. Automated Inference and Theorem proving. Logical inference methods. Derivation and proof. Rules of inference. Formal proofs. The Fitch System. Semantic Tableau. Resolution in Propositional Calculus. Dual Resolution. [18.03.2020 (online course; lecture 3 below)]
5. The role of CNF. The SAT problem. Approaches to solving the SAT problem. Decision trees. OBDD diagrams. SAT solvers. [25.03.2020; lecture 4 below]
6. Logical consequence and logical equivalence. Transformations of formulas: equivalence transformation rules. Minterms and maxterms. Normal forms: CNF, DNF, NNF. Implicants and implicents. Maximal and minimal representation of CNF and DNF. What is the real meaning of CNF and DNF? [Czwartek, 2.04.2020, 12:00-14:00; ALi - on-line, via UPEL/ClickMeeting]
7. 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]
8. Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT [Czwartek, 23.04.2020, 12:00-14:00; ALi - on-line, via UPEL/ClickMeeting]
9. 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.
10. 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]
11. 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]
12. Introduction to logic programming. Prolog. Constraint Programming. Multi-valued logics. Fuzzy logic. Temporal and modal logics. Description logics.

Yet another chance:

On-line Logic Course - recommended

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

1. An Introduction to Logic
2. Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF [ Support material for Lecture 3 : Czwartek, 2.04.2020, start godz. 12:00]
3. Propositional Calculus: Syntax, Sematics, Equivalence, CNF, DNF [Update: 15-04-2020]
4. 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]
5. Propositional Calculus: Theorem Proving, Inference Rules, Resolution, Dual Resolution, Semantic Tableau, Fitch [Update: 15-04-2020]
6. Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT
7. Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT [Update: 22/23-04-2020]
8. Predicate Calculus: Introduction, Syntax, Semantics. Variables, Terms, Quantifiers. Logical Formulas and their Interpretation [Update: 29/30-04-2020]
9. Predicate calculus: Syntax, Semantics, Herbrand Interpretation, Transformation Rules, Inference Rules, Resolution and Dual Resolution [Update: 6/7-05-2020]
10. Example of Resolution Proof: Marcus&Cesar
11. 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))

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

—- Egzaminy 2018:

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

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

—- Egzaminy 2017:

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

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

Egzaminy 2016:

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

Materiały pomocnicze do wykładu:

Materiał uzupełniający

Logika-1: Wprowadzenie do logiki

Logika-2-3: Podstawy rachunku zdań

Logika-4: Dowodzenie w rachunku zdań

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

Podstawy syntezy układów logicznych

Wykład KJo 1 i 2

Wykład KJo zaawansowany

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

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

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

Wykłady - 2014

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

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

1. logika-intro-1-3-2014

Polecane materiały - e-learning

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

Wykłady - 2013

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

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

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

Polecane materiały - e-learning

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

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

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

Plan ćwiczeń - 2014

1. Różne rozmaitości, czyli wprowadzenie do logiki w przededniu. Algebra zbiorów.
2. Rachunek zdań. Podstawy. Składnia, semantyka, badanie własności formuł.
3. Rachunek zdań. Przekształcenia równoważne. Postacie CNF, DNF, NNF. Synteza układów logicznych.
4. Rachunek zdań. Dowodzenie twierdzeń.
5. Rachunek pierwszego rzędu. Składnia, semantyka, przykłady. Wprowadzenie do metody rezolucji.
6. Rachunek pierwszego rzędu. Dowodzenie. Rezolucja.

Sylabus

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

Materiały pomocnicze

Linki

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