(August-December 2006)

Instructor: |
Paritosh K. Pandya Room A249 Phone: (tifr) Ext. 2551 Email: pandya@tifr.res.in |

Time: |
Tuesday & Thursday: 11:30 to 13:00
Room No.
A 212 |

Course Page | http://www.tcs.tifr.res.in/~pandya/logic06/index.html |

Google Group |
logictifr06@googlegroups.com |

Mathematical Preliminaries: Set, Relations, Partial Orders, Well-ordered sets and principle of Noetherian induction, Structural induction, Cardinality of Sets.

Propositional Calculus:

Syntax and semantics

Hintikka's Lemma and Model Existence Theorem

Model theory: Compactness, Lowenheim-skolem theorem, normal forms, functional completeness

Semantic Tablaeux: soundness, completeness and decidability

Hilbert style proof system, Sequent calculusFirst-order logic:

Syntax and semantics

Hintikka's Lemma and model existence theorem

First-order semantic Tableaux: soundness and completeness

Hilbert style proof system for FOL, deduction theorem, Sequent calculus

Prenex normal form, ResolutionFirst-order logic with equality:

Canonical models, Model existence theorem

Axiomatisation and completeness

Upward and downward Lowenheim-Skolem Theorems*** OMITTED Scope of First-order Logic:

Axiomatisation of some mathematical structures

ZFC set theory in FOL, Limitations of FOLDecision procedures: quantifier-free formulae with uninterpreted functions with equality, theory of lists and arrays, First order real-arithmetic, Fourier-Motzkin Variable Elimination Basics of Modal and Program Logics: Kripke semantics, Correspondances, Axiomatisation: systems K, KT4, S5, completeness, decidability using filteration. Dynamic logic: axiomatisation and completeness.

J.H. Gallier: Logic for computer science, John Wiley and Sons, 1987. M. Fitting: First-order logic and automated theorem proving, Springer-Verlag, 1990. H.D. Ebbinghaus, J. Flum, W. Thomas: Mathematical Logic, Springer-Verlag, 1984.

Assignment 5 (manoj topics)

Decision Procedures (Manoj Raut)

Notes on Modal Logics (R. Ramanujam)