E0 205 Mathematical Logic and Theorem Proving

• Course outline
  • Propositional Logic
    • Semantic Tableau and Resolution
    • Hilbert and Gentzen style axiom system
    • Completeness
    • Compactness
  • First-order Logic
    • Syntax, semantics
    • Compactness and Lowenheim-Skolem Theorem
    • Semantic Tableaux and Resolution, completeness
    • Ehrenfeucht-Fraisse Games

• Texts and other material:
  • "First-order Logic and automated theorem proving", Melvin Fitting, Springer-Verlag, 1990.
  • "Logic for Computer Science -- Foundations for Automatic Theorem Proving", Jean H. Gallier.
  • "Mathematical Logic", Ebbinghaus, Flum, Thomas, Springer UTM.
  • "An introduction to Logic", Madhavan Mukund (lecture notes).

• Assignments
  • Assignment 1.
  • Assignment 2.
  • Assignment 3.
  • Assignment 4.
  • Assignment 5.

• Seminar topics
  1. SAT Solvers: Joy Chakraborty, 3:30pm Fri 10 Sep 2004.
  2. Modal Logic: Pavithra Prabhakar.
  3. Hilbert style axiom system for propositional logic: K. R. Raghavendra, 3:30pm Fri 24 Sep 2004.
  4. Buchi's Theorem on Monadic Second Order Logic and Automata: Arul Ganesh 3:30pm Fri 29 Oct 2004.
  5. Undecidability of First-Order Logic: Debamalya Panigrahi, 3:30pm Fri 5th Nov 2004.
  6. Descriptive Complexity: Madhu Gopinathan, 3:30pm Wed 10 Nov 2004.
  7. Gentzen's Cut Elimination Theorem: Gaurav Malhotra, 3:30pm Wed 17 Nov 2004.
  8. Logic and Set Theory: P. Sivaram Prasad, 3:30pm Fri 19 Nov 2004.
  9. Ehrenfeucht-Fraisse Games - I: Mangesh Gupte, 3:30pm Fri 26 Nov 2004.
  10. Ehrenfeucht-Fraisse Games - II: Mangesh Gupte, 11:30am Mon 29 Nov 2004.
  11. First-order logic with equality: Raj Mohan, 3:30pm Wed 1 Dec 2004.

• Proposed weightage for evaluation:
  • Mid-semester Exam: 20%
  • Assignments (Lab + written) and Seminars: 40%
  • Final Exam: 40%

• Meeting schedule: Tue & Thu, 2:00pm, in CSA Seminar Room.

• Exam Schedule:
  • Mid-semester Exam:
  • Final Exam: