I read on Wikipedia that unification is a process of solving the satisfability problem. At the same time, I know that such solvers are called "SAT solvers" or "SMT solvers". So, are they different ...
I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...