CS41105: Symbolic Logic And Automated Reasoning
| CS41105 | |
|---|---|
| Course name | Symbolic Logic And Automated Reasoning |
| Offered by | Computer Science & Engineering |
| Credits | 3 |
| L-T-P | 3-0-0 |
| Previous Year Grade Distribution | |
| {{{grades}}} | |
| Semester | Autumn |
Syllabus[edit | edit source]
Syllabus mentioned in ERP[edit | edit source]
Introduction and motivation: Role of logic in Computer Science, problem representation.Basic notions: language, models, interpretations, validity, proof, decision problems in logic. decidability.Propositional logic: Syntax, semantics, proof systems, Validity, satisfiability and unsatisfiability, soundness and completeness.Machinasation: truth tables, normal forms, semantic tableaux, resolution, proof by contradiction, example.First order predicate logic theory: Quantifiers, first order models, validity and satisfiability, semantic tableaux.Normal forms, skolemization: elimination of quantifiers, unification, resolution and various resolution strategies, equality axioms and paramodulation. Horn formulas and programs. Prolog as a restricted resolutionbased theorem prover. Undecidability and incompleteness in logic, compactness Theorem.Other topics: Introduction to Modal Logic, Temporal Logic and other logics for concurrency. Some exposure to theorem proving systems such as Prolog, PVS, SPIN, etc.References1.Michael Huth and Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press.2.Arindama Singh, Logics for Computer Science, Prentice Hall of India.3.C. L. Chang and R. C. T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press.4.M. Ben-Ari, Mathematical Logic for Computer Science, Springer.5.E. Mendelson, Introduction to Mathematical Logic, Chapman and Hall.