Pattern Matching on Logic Variables
← Back to Unification
Unification finds substitutions that make two terms equal, binding logic variables in the process. Unlike pattern matching in functional languages, unification is bidirectional — both sides can contain variables, and the algorithm finds the most general unifier.