(55 minutes to learn)
Unification is a procedure which takes two symbolic expressions containing variables, and returns a substitution to the variables which makes the expressions identical. It is a key component of first-order theorem provers and type inference systems.
This concept has the prerequisites:
- first-order logic (Unification is a commonly used operation in first order reasoning.)
- Know what the unification procedure is and what the output is.
- Be able to simulate it on simple examples.
- What is the occurs check, why is it needed, and why does it increase the complexity of the algorithm?
- Why do variables sometimes need to be renamed before performing unification?
- What does it mean for one unifier to be more general than another, and why does one desire the most general unifier?
-No Additional Notes-
- create concept: shift + click on graph
- change concept title: shift + click on existing concept
- link together concepts: shift + click drag from one concept to another
- remove concept from graph: click on concept then press delete/backspace
- add associated content to concept: click the small circle that appears on the node when hovering over it
- other actions: use the icons in the upper right corner to optimize the graph placement, preview the graph, or download a json representation