Lecture 8 of 42Mathematical Logic
More Informal Proofs
Prof. Arindama Singh · IIT Madras
Credits and licence
- From
- Mathematical Logic, IIT Madras (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
- Sets and Strings
- Syntax of Propositional Logic
- Unique Parsing
- Semantics of PL
- Consequences and Equivalences
- Five results about PL
- Calculations and Informal Proofs
- More Informal Proofs
- Normal forms
- SAT and 3SAT
- Horn-SAT and Resolution
- Resolution
- Adequacy of Resolution
- Adequacy and Resolution Strategies
- Propositional Calculus (PC)
- Some Results about PC
- Arguing with Proofs
- Adequacy of PC
- Compactness & Analytic Tableau
- Examples of Tableau Proofs
- Adequacy of Tableaux
- Syntax of First order Logic (FL)
- Symbolization & Scope of Quantifiers
- Hurdles in giving Meaning
- Semantics of FL
- Relevance Lemma
- Validity, Satisfiability & Equivalence
- Six Results about FL
- Laws in FL
- Quantifier Laws and Consequences
- Examples of Informal Proofs and Calculation
- Prenex Form Conversion
- Skolem Form
- Syntatic Interpretation
- Herbrand's Theorem
- Most General Unifiers
- Resolution Rules
- Resolution Examples
- Axiomatic System FC
- FC, Semidecidability of FL, and Tableau
- Analytic Tableau for FL
- Goedel's Incompleteness Theorems