Reading Logic, Feb 2018*
Course
Prince Mathew reads and presents various topics in Logic.
Book
Logic in Computer Science by Huth and Ryan (H&R)
Artificial Intelligence by Russel Norwig(RN)
Syllabus
Prince Mathew reads and presents various topics in Logic.
Book
Logic in Computer Science by Huth and Ryan (H&R)
Artificial Intelligence by Russel Norwig(RN)
Syllabus
| # | Date | Content | References |
|---|---|---|---|
| 1 | 14-02-2018 | Declarative sentences, Natural deduction, Provable equivalence, Well Formed Formulas | H&R1.1, 1.2, 1.3 |
| 2 | 16-02-2018 | Semantics of propositional logic, Soundness & Completeness- Introduction | H&R1.4 |
| 3 | 19-02-2018 | Soundness of Propositional logic | H&R1.4 |
| 4 | 20-02-2018 | Completeness of Propositional logic | H&R1.4 |
| 5 | 06-03-2018 | Normal forms - Semantic equivalence, Satisfiablility and Validity, CNF and Validity | H&R1.5 |
| 6 | 07-03-2018 | Horn Clauses and Satisfibility | H&R1.5 |
| 7 | 08-03-2018 | SAT solvers- Linear solver, Cubic solver | H&R1.6 |
| 8 | 15-03-2018 | Effective propositional model checking, Unit propagation, Pure literal elimination, DPLL Algorithm | RN7.6, Wikipedia |
| 9 | 16-03-2018 | The Wumpus World, Agents based on propositional logic, Hybrid agent, Logical state estimation | RN7.2,7.7 |
| 10 | 19-03-2018 | Propositional Theorem Proving, Inference and Proofs, Proof by resolution, Horn clauses and Definite clauses, Forward and Backward chaining | RN7.5 |
| 11 | 26-03-2018 | Predicate Logic- The need for richer language | H&R2.1 |
| 12 | 27-03-2018 | Predicate logic as a formal language- Terms, Formulas, Free and Bound variables, Substitution | H&R2.2 |
| 13 | 28-03-2018 | Proof theory of predicate logic- Natural deduction rules, Quatifier equivalences, Semantics of predicate logic- Models, Semantic Entailment, Semantics of equality | H&R2.3,2.4 |
| 14 | 11-04-2018 | Micromodels of software- State Machines, Case Study- Alma | H&R2.7 |
| 15 | 17-04-2018 | A Software Micromodel | H&R2.7 |
| 16 | 18-04-2018 | Program Verification- Need for verification, Framework for software verification, Hoare triples | H&R4.1,4.2 |
| 17 | 30-04-2018 | Partial and Total correctness, Program variables and Logical variables, Proof calculus for partial correctness, Proof tableaux | H&R4.3 |
| 18 | 02-05-2018 | Case Study Minimal-Sum section, Proof calculus for total correctness, Programming by contract | H&R4.3,4.4,4.5 |