First-order logic basics
Artificial Intelligence · Engineering
Study notes
Express: Every human is mortal. First-order: forall x (Human(x) -> Mortal(x)). Fact: Human(Socrates). Inference: substitute x=Socrates, modus ponens gives Mortal(Socrates). Unification matches Loves(x,y) with Loves(John,Mary) binding x=John. Resolution proves by contradiction, powering Prolog.