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

Syllabus mentioned in ERP

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.