E0 205 Mathematical Logic and Theorem Proving
- Semantic Tableau and Resolution
- Hilbert and Gentzen style axiom system
- 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,
- "Logic for Computer Science -- Foundations for Automatic
Theorem Proving", Jean H. Gallier.
"Mathematical Logic", Ebbinghaus, Flum, Thomas, Springer
"An introduction to Logic",
Madhavan Mukund (lecture notes).
- Seminar topics
SAT Solvers: Joy Chakraborty, 3:30pm Fri 10 Sep 2004.
Modal Logic: Pavithra Prabhakar.
Hilbert style axiom system for
propositional logic: K. R.
Raghavendra, 3:30pm Fri 24 Sep 2004.
- Buchi's Theorem on
Monadic Second Order Logic and Automata: Arul Ganesh 3:30pm Fri 29 Oct 2004.
of First-Order Logic: Debamalya Panigrahi,
3:30pm Fri 5th Nov 2004.
Complexity: Madhu Gopinathan, 3:30pm Wed 10 Nov
Gentzen's Cut Elimination Theorem: Gaurav Malhotra, 3:30pm
Wed 17 Nov 2004.
Logic and Set Theory: P. Sivaram Prasad, 3:30pm Fri 19 Nov 2004.
Ehrenfeucht-Fraisse Games - I: Mangesh Gupte, 3:30pm Fri 26 Nov 2004.
Ehrenfeucht-Fraisse Games - II: Mangesh Gupte, 11:30am Mon
29 Nov 2004.
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
- Exam Schedule: