e-Learn @ SASTRA Back

Introduction - Syllabus overview

Foundations of logics and proofs

Proof using TT, DeMorgan's laws

Satisfiability of propositional formulas

Validity of formula - Interpretations

Satisfiability of formulas - theorems and proofs

Satisfiability using semantic tableaux

Analysis of satisfiability using semantic tableaux

Properties of decision procedures

Soundness and completeness

Hintikka set

Hintikka's lemma - proof

Ground Resolution Rule

DP Algorithm

Satisfiability using semantic tableaux - problems

Partial Interpretation

DPLL algorithm

Revision of Unit-1 portions

N-queens problem

N-queens problem- contd

Deductive systems for PL - Gentzen system

Gentzen system

Hilbert system

Skolem's algorithm

Skolem's algorithm

First order Logic - basics

First order Logic - interpretations

FOL - Herbrand model

Substitution - Composition

General Resolution Procedure

Soundness of resolution

Lifting Lemma - Proof

Temporal logic

Operators of PTL

State transition diagrams

Deductive system - L for temporal logic

Hoare logic

Scheduling algorithms

Correctness of concurrent programs

Lambda calculus - introduction


Free, bound and binding variables

Substitution in lambda

Substitution - problems

Substitution - problems

Substitution - Lemma and proof

Beta reduction

Beta reduction

Beta equality

Beta equality - problems

Combinatory logic - introduction

Substitution in CL

Substitution in CL - problems

Reduction in CL

Reduction in CL - problems

Reduction in CL - problems

Lambda and combinators - fixed point theorem

Primitive recursive functions