## 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**

# | 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 |