E0 205 Mathematical Logic and Theorem Proving

Course outline

Propositional Logic
 Semantic Tableau and Resolution
 Hilbert and Gentzen style axiom system
 Completeness
 Compactness
 Firstorder Logic
 Syntax, semantics
 Compactness and LowenheimSkolem Theorem
 Semantic Tableaux and Resolution, completeness
 EhrenfeuchtFraisse Games
 Texts and other material:

"Firstorder Logic and automated theorem proving", Melvin Fitting,
SpringerVerlag, 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
 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.

Undecidability
of FirstOrder Logic: Debamalya Panigrahi,
3:30pm Fri 5th Nov 2004.

Descriptive
Complexity: Madhu Gopinathan, 3:30pm Wed 10 Nov
2004.

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.

EhrenfeuchtFraisse Games  I: Mangesh Gupte, 3:30pm Fri 26 Nov 2004.

EhrenfeuchtFraisse Games  II: Mangesh Gupte, 11:30am Mon
29 Nov 2004.

Firstorder logic with equality: Raj
Mohan, 3:30pm Wed 1 Dec 2004.

Proposed weightage for evaluation:

Midsemester Exam: 20%

Assignments (Lab + written) and Seminars: 40%

Final Exam: 40%

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

Midsemester Exam:

Final Exam: