Harvard's CS50 AI (in a nutshell)
This week I completed Harvard's CS50's Artificial Intelligence course, and with it having been only half as long as CS50x, I’m left a bit heartbroken that it’s already over. Never the less the whole course was packed with new intriguing concepts, and so here is a quick summary of what amazing things the course includes:
You start with uninformed search algorithms such as DFS and BFS, then explore informed search using heuristics: Greedy Best-First Search and A*. You also see how these show up in games (e.g., Tic-Tac-Toe) via the Minimax algorithm, plus improvements like alpha–beta pruning and depth-limited minimax with an evaluation function. I've written all about how the first week was in another blog - check that out if you want to dive deeper!
Week 1 introduces knowledge-based agents: agents that reason over a knowledge base (KB) of sentences (assertions about the world in a knowledge representation language). A model is an assignment of a truth value to every proposition (i.e., a possible state of the world). You meet entailment and inference—deriving new sentences from old ones. Then you dig into propositional logic: negation, conjunction, disjunction (including exclusive OR), implication, and biconditionals. You learn how model checking can be used to decide entailment. From there, you do knowledge engineering to represent real problems like Cluedo/Clue or Mastermind. You also see common inference rules: Modus Ponens, ∧-elimination, double negation, implication, elimination biconditional elimination, De Morgan’s laws, and distributivity. Next is resolution with proof by contradiction, which works by converting propositions to conjunctive normal form (CNF). To do this: 1. eliminate biconditionals, 2.eliminate implications, 3. push negations inward so only literals are negated (via De Morgan’s), 4.distribute to get a conjunction of clauses. During resolution you factor (remove duplicate literals in a clause). If you eventually derive the empty clause you’ve reached a contradiction. Finally, you meet First-Order Logic (FOL), which expresses complex ideas more succinctly than propositional logic using constant symbols (objects) and predicate symbols (relations/properties). FOL adds quantifiers: Universal Quantification uses the symbol ∀x to express "for all symbols x", and in Existential Quantification the symbol ∃x expresses that "there is at least one symbol where" some condition is true.