Lecture 31 of 39Module 1
Resolution : Soundness and Completeness
Prof. S. Arun Kumar · IIT Delhi
Credits and licence
- From
- Logic for CS, IIT Delhi (at NPTEL)
- Licence
- CC BY-NC-SA, as NPTEL states it. Non-commercial use only.
- Attribution
- NPTEL states: "Distributed under Creative Commons Attribution-ShareAlike / CC BY - NC - SA", beside a BY-NC-SA badge.
- Who can watch
- Tweens profiles and older. How courses are placed
All the lectures
- Introduction
- Propositional Logic Syntax
- Semantics of Propositional Logic
- Logical and Algebraic Concepts
- Identities and Normal forms
- Tautology Checking
- Propositional Unsatisfiability
- Analytic Tableaux
- Consistency and Completeness
- The Completeness Theorem
- Maximally Consistent Sets
- Formal Theories
- Proof Theory : Hilbert-style
- Derived Rules
- The Hilbert System : Soundness
- The Hilbert System :Completeness
- Introduction to Predicate Logic
- The Semantic of Predicate Logic
- Subsitutions
- Models
- Structures and Substructures
- First - Order Theories
- Predicate Logic: Proof Theory (Contd..)
- Existential Quantification
- Normal Forms
- Skalemization
- Substitutions and Instantiations
- Unification
- Resolution in FOL
- More on Resolution in FOL
- Resolution : Soundness and Completeness
- Resolution and Tableaux
- Completeness of Tableaux Method
- Completeness of the Hilbert System
- First -Order Theories
- Towards Logic Programming
- Verification of Imperative Programs
- Verification of WHILE Programs
- References