Różnice między wybraną wersją a wersją aktualną.
| Both sides previous revision Poprzednia wersja Nowa wersja | Poprzednia wersja Nowa wersja Both sides next revision | ||
|
pl:dydaktyka:logic:start [2020/03/18 09:32] ligeza [Logic for Computer Science: 2020] |
pl:dydaktyka:logic:start [2020/04/01 13:03] ligeza [Logic for Computer Science: 2020] |
||
|---|---|---|---|
| Linia 10: | Linia 10: | ||
| - **<fc #4682b4>Logical equivalence. Transformations of formulas: equivalent transformation rules. Minterms and maxterms. Normal forms: CNF, DNF, NNF. Implicants and implicents. Minimal representation.</fc>** [11.03.2020 (online course; lecture 2 below)] | - **<fc #4682b4>Logical equivalence. Transformations of formulas: equivalent transformation rules. Minterms and maxterms. Normal forms: CNF, DNF, NNF. Implicants and implicents. Minimal representation.</fc>** [11.03.2020 (online course; lecture 2 below)] | ||
| - **<fc #4682b4>Automated Inference and Theorem proving. Logical inference methods. Derivation and proof. Rules of inference. Formal proofs. The Fitch System. Semantic Tableau. Resolution in Propositional Calculus. Dual Resolution.</fc>** [18.03.2020 (online course; lecture 3 below)] | - **<fc #4682b4>Automated Inference and Theorem proving. Logical inference methods. Derivation and proof. Rules of inference. Formal proofs. The Fitch System. Semantic Tableau. Resolution in Propositional Calculus. Dual Resolution.</fc>** [18.03.2020 (online course; lecture 3 below)] | ||
| - | - The role of CNF. The SAT problem. Approaches to solving the SAT problem. Decision trees. OBDD diagrams. SAT solvers. | + | - **<fc #4682b4>The role of CNF. The SAT problem. Approaches to solving the SAT problem. Decision trees. OBDD diagrams. SAT solvers.</fc>** [25.03.2020; lecture 4 below] |
| + | - <fc #ff00ff>Logical consequence and logical equivalence. Transformations of formulas: equivalence transformation rules. Minterms and maxterms. Normal forms: CNF, DNF, NNF. Implicants and implicents. Maximal and minimal representation of CNF and DNF. What is the real meaning of CNF and DNF?</fc> [1.04.2020; 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 systnthesis. Karnaugh Tables. The Quine-McCluskey algorithm. | - Boolean Algebra. Function syntehsis. The CNF and DNF again: the Pi and Sigma notations. Finding minimal representations. Logical circuits systnthesis. Karnaugh Tables. The Quine-McCluskey algorithm. | ||
| - First -Order Logic. Syntax and Semantix. Logical transformation Rules. Logical inference rules. The Fitch system for FOPC. | - First -Order Logic. Syntax and Semantix. Logical transformation Rules. Logical inference rules. The Fitch system for FOPC. | ||
| Linia 24: | Linia 25: | ||
| - {{:pl:dydaktyka:logic:logic_for_computer_science_2020.pdf | An Introduction to Logic}} | - {{:pl:dydaktyka:logic:logic_for_computer_science_2020.pdf | An Introduction to Logic}} | ||
| - | - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-2.pdf | Propositional Calculus: Synatx, Sematix, Equivalence, CNF, DNF}} | + | - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-2.pdf | Propositional Calculus: Synatx, Sematics, Equivalence, CNF, DNF }} [ <fc #ff00ff>Support material for Lecture 6</fc> : Czwartek, 2.04.2020, start godz. 12:00] |
| - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-3.pdf | Propositional Calculus: Theorem Proving}} | - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-3.pdf | Propositional Calculus: Theorem Proving}} | ||
| + | - {{ :pl:dydaktyka:logic:logic_for_computer_science_2020-4.pdf | Propositional Calculus: Model Analysis: Decision Trees, OBDD, and SAT}} | ||
