Knowledge — Propositional Logic, Model Checking, Inference Rules & Knowledge Representation | Harvard CS50 AI Week 1
Week 1 is about getting a program to derive new facts from known ones: propositional symbols and five connectives turn knowledge into sentences; model checking enumerates all 2^n truth assignments to decide whether the knowledge base entails a query; inference rules and resolution work on the sentences directly, converting to CNF and deriving the empty clause by contradiction; first-order logic cuts the number of symbols with constants, predicates and quantifiers. With time links for every section, plus the approach, common mistakes and self-checks for the Knights and Minesweeper projects (reference implementations folded away).