The basic idea is we want to check if a formula $\varphi$ is satisfiable. This is analogous to checking there exists a row in the truth-table for a proposition for which the proposition is true. First-order logic is not as simple as "write down the truth-table", because it requires constructing a model and an interpretation.
Recall, there are three related notions:
- Unsatisfiability means there is no interpretation for which $\varphi$ holds
- Validity means $\varphi$ holds in every interpretation
- Satisfiability means there is at least one interpretation for which $\varphi$ holds.
A common trick to proving $\varphi$ is satisfiable is to try to prove its negation $\neg\varphi$ is unsatisfiable.
Another common trick is to transform our formula $\varphi$ into an equisatisfiable form like conjunctive normal form. Conjunctive normal form is useful for proving a formula is valid...but if $\neg\varphi$ is valid, then $\varphi$ is unsatisfiable. So we want to prove $\neg\varphi$ is not valid, which can be done quickly and efficiently.
For a detailed walkthrough about this process, John Harrison's Handbook of Practical Logic and Automated Reasoning discusses this in chapter 2, section 6 et seq.